Metamath Proof Explorer

Theorem meran3

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

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

Proof

Step Hyp Ref Expression
1 pm2.3 
 |-  ( ( ch \/ ( th \/ ta ) ) -> ( ch \/ ( ta \/ th ) ) )
2 1 imim2i 
 |-  ( ( ( -. ph \/ ps ) -> ( ch \/ ( th \/ ta ) ) ) -> ( ( -. ph \/ ps ) -> ( ch \/ ( ta \/ th ) ) ) )
3 pm1.5 
 |-  ( ( ch \/ ( ta \/ th ) ) -> ( ta \/ ( ch \/ th ) ) )
4 2 3 syl6 
 |-  ( ( ( -. ph \/ ps ) -> ( ch \/ ( th \/ ta ) ) ) -> ( ( -. ph \/ ps ) -> ( ta \/ ( ch \/ th ) ) ) )
5 imor 
 |-  ( ( ( -. ph \/ ps ) -> ( ch \/ ( th \/ ta ) ) ) <-> ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) )
6 imor 
 |-  ( ( ( -. ph \/ ps ) -> ( ta \/ ( ch \/ th ) ) ) <-> ( -. ( -. ph \/ ps ) \/ ( ta \/ ( ch \/ th ) ) ) )
7 4 5 6 3imtr3i 
 |-  ( ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) -> ( -. ( -. ph \/ ps ) \/ ( ta \/ ( ch \/ th ) ) ) )
8 meran1 
 |-  ( -. ( -. ( -. ph \/ ps ) \/ ( ta \/ ( ch \/ th ) ) ) \/ ( -. ( -. ch \/ ph ) \/ ( ta \/ ( th \/ ph ) ) ) )
9 8 imorri 
 |-  ( ( -. ( -. ph \/ ps ) \/ ( ta \/ ( ch \/ th ) ) ) -> ( -. ( -. ch \/ ph ) \/ ( ta \/ ( th \/ ph ) ) ) )
10 7 9 syl 
 |-  ( ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) -> ( -. ( -. ch \/ ph ) \/ ( ta \/ ( th \/ ph ) ) ) )
11 10 imori 
 |-  ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. ch \/ ph ) \/ ( ta \/ ( th \/ ph ) ) ) )