Metamath Proof Explorer

Theorem df3an2

Description: Express triple-and in terms of implication and negation. Statement in Frege1879 p. 12. (Contributed by RP, 25-Jul-2020)

Ref Expression
Assertion df3an2 ⊢ φ ∧ ψ ∧ χ ↔ ¬ φ → ψ → ¬ χ

Proof

Step Hyp Ref Expression
1 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
2 df-an ⊢ φ ∧ ψ ∧ χ ↔ ¬ φ ∧ ψ → ¬ χ
3 impexp ⊢ φ ∧ ψ → ¬ χ ↔ φ → ψ → ¬ χ
4 2 3 xchbinx ⊢ φ ∧ ψ ∧ χ ↔ ¬ φ → ψ → ¬ χ
5 1 4 bitri ⊢ φ ∧ ψ ∧ χ ↔ ¬ φ → ψ → ¬ χ