Metamath Proof Explorer

Theorem meran2

Description: A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011)

Ref Expression
Assertion meran2 
|- ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. ta \/ th ) \/ ( ch \/ ( ph \/ th ) ) ) )

Proof

Step Hyp Ref Expression
1 meran1 
 |-  ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
2 1 imorri 
 |-  ( ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) -> ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
3 meran1 
 |-  ( -. ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) \/ ( -. ( -. ta \/ th ) \/ ( ch \/ ( ph \/ th ) ) ) )
4 3 imorri 
 |-  ( ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) -> ( -. ( -. ta \/ th ) \/ ( ch \/ ( ph \/ th ) ) ) )
5 2 4 syl 
 |-  ( ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) -> ( -. ( -. ta \/ th ) \/ ( ch \/ ( ph \/ th ) ) ) )
6 5 imori 
 |-  ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. ta \/ th ) \/ ( ch \/ ( ph \/ th ) ) ) )