Metamath Proof Explorer


Theorem 19.43

Description: Theorem 19.43 of Margaris p. 90. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 27-Jun-2014)

Ref Expression
Assertion 19.43 x φ ψ x φ x ψ

Proof

Step Hyp Ref Expression
1 df-or φ ψ ¬ φ ψ
2 1 exbii x φ ψ x ¬ φ ψ
3 19.35 x ¬ φ ψ x ¬ φ x ψ
4 alnex x ¬ φ ¬ x φ
5 4 imbi1i x ¬ φ x ψ ¬ x φ x ψ
6 2 3 5 3bitri x φ ψ ¬ x φ x ψ
7 df-or x φ x ψ ¬ x φ x ψ
8 6 7 bitr4i x φ ψ x φ x ψ