Metamath Proof Explorer


Theorem 19.43OLD

Description: Obsolete proof of 19.43 . Do not delete as it is referenced on the mmrecent.html page and in conventions-labels . (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 19.43OLD xφψxφxψ

Proof

Step Hyp Ref Expression
1 ioran ¬φψ¬φ¬ψ
2 1 albii x¬φψx¬φ¬ψ
3 19.26 x¬φ¬ψx¬φx¬ψ
4 alnex x¬φ¬xφ
5 alnex x¬ψ¬xψ
6 4 5 anbi12i x¬φx¬ψ¬xφ¬xψ
7 2 3 6 3bitri x¬φψ¬xφ¬xψ
8 7 notbii ¬x¬φψ¬¬xφ¬xψ
9 df-ex xφψ¬x¬φψ
10 oran xφxψ¬¬xφ¬xψ
11 8 9 10 3bitr4i xφψxφxψ