Metamath Proof Explorer

Theorem orim12dALT

Description: Alternate proof of orim12d which does not depend on df-an . This is an illustration of the conservativity of definitions (definitions do not permit to prove additional theorems whose statements do not contain the defined symbol). (Contributed by Wolf Lammen, 8-Aug-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses orim12dALT.1 φ ψ χ
orim12dALT.2 φ θ τ
Assertion orim12dALT φ ψ θ χ τ


Step Hyp Ref Expression
1 orim12dALT.1 φ ψ χ
2 orim12dALT.2 φ θ τ
3 pm2.53 ψ θ ¬ ψ θ
4 1 con3d φ ¬ χ ¬ ψ
5 4 2 imim12d φ ¬ ψ θ ¬ χ τ
6 pm2.54 ¬ χ τ χ τ
7 3 5 6 syl56 φ ψ θ χ τ