On Mon, Mar 15, 2021 at 3:02 PM Mario Carneiro <[email protected]> wrote:
> which we can substitute in the current setting to: > ((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))), > ((B ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))), > F(B) > ⊢ F((A ∧ F) ∨ (B ∧ ¬ F)) > Amendment: ((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))), ((B ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(B) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))), F(B) ⊢ F((A ∧ F) ∨ (B ∧ ¬ F)) > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStFMZXzyV8fJeQmobWuGNK%2Bc8dQocT5_4LrHS1frBqhaA%40mail.gmail.com.
