Metamath Proof Explorer

Theorem meran1

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

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

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( -. ph -> ( -. ph \/ ps ) )
2 olc 
 |-  ( ps -> ( -. ph \/ ps ) )
3 1 2 ja 
 |-  ( ( ph -> ps ) -> ( -. ph \/ ps ) )
4 3 imim1i 
 |-  ( ( ( -. ph \/ ps ) -> ( ch \/ ( th \/ ta ) ) ) -> ( ( ph -> ps ) -> ( ch \/ ( th \/ ta ) ) ) )
5 pm2.24 
 |-  ( th -> ( -. th -> ph ) )
6 idd 
 |-  ( th -> ( ph -> ph ) )
7 5 6 jaod 
 |-  ( th -> ( ( -. th \/ ph ) -> ph ) )
8 7 com12 
 |-  ( ( -. th \/ ph ) -> ( th -> ph ) )
9 pm1.5 
 |-  ( ( -. ( ph -> ps ) \/ ( ch \/ ( th \/ ta ) ) ) -> ( ch \/ ( -. ( ph -> ps ) \/ ( th \/ ta ) ) ) )
10 pm2.3 
 |-  ( ( -. ( ph -> ps ) \/ ( th \/ ta ) ) -> ( -. ( ph -> ps ) \/ ( ta \/ th ) ) )
11 pm1.5 
 |-  ( ( -. ( ph -> ps ) \/ ( ta \/ th ) ) -> ( ta \/ ( -. ( ph -> ps ) \/ th ) ) )
12 pm2.21 
 |-  ( -. ph -> ( ph -> ps ) )
13 jcn 
 |-  ( th -> ( -. ph -> -. ( th -> ph ) ) )
14 12 13 imim12i 
 |-  ( ( ( ph -> ps ) -> th ) -> ( -. ph -> ( -. ph -> -. ( th -> ph ) ) ) )
15 14 pm2.43d 
 |-  ( ( ( ph -> ps ) -> th ) -> ( -. ph -> -. ( th -> ph ) ) )
16 15 con4d 
 |-  ( ( ( ph -> ps ) -> th ) -> ( ( th -> ph ) -> ph ) )
17 imor 
 |-  ( ( ( ph -> ps ) -> th ) <-> ( -. ( ph -> ps ) \/ th ) )
18 imor 
 |-  ( ( ( th -> ph ) -> ph ) <-> ( -. ( th -> ph ) \/ ph ) )
19 16 17 18 3imtr3i 
 |-  ( ( -. ( ph -> ps ) \/ th ) -> ( -. ( th -> ph ) \/ ph ) )
20 19 orim2i 
 |-  ( ( ta \/ ( -. ( ph -> ps ) \/ th ) ) -> ( ta \/ ( -. ( th -> ph ) \/ ph ) ) )
21 pm1.5 
 |-  ( ( ta \/ ( -. ( th -> ph ) \/ ph ) ) -> ( -. ( th -> ph ) \/ ( ta \/ ph ) ) )
22 10 11 20 21 4syl 
 |-  ( ( -. ( ph -> ps ) \/ ( th \/ ta ) ) -> ( -. ( th -> ph ) \/ ( ta \/ ph ) ) )
23 22 orim2i 
 |-  ( ( ch \/ ( -. ( ph -> ps ) \/ ( th \/ ta ) ) ) -> ( ch \/ ( -. ( th -> ph ) \/ ( ta \/ ph ) ) ) )
24 pm1.5 
 |-  ( ( ch \/ ( -. ( th -> ph ) \/ ( ta \/ ph ) ) ) -> ( -. ( th -> ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
25 9 23 24 3syl 
 |-  ( ( -. ( ph -> ps ) \/ ( ch \/ ( th \/ ta ) ) ) -> ( -. ( th -> ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
26 imor 
 |-  ( ( ( ph -> ps ) -> ( ch \/ ( th \/ ta ) ) ) <-> ( -. ( ph -> ps ) \/ ( ch \/ ( th \/ ta ) ) ) )
27 imor 
 |-  ( ( ( th -> ph ) -> ( ch \/ ( ta \/ ph ) ) ) <-> ( -. ( th -> ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
28 25 26 27 3imtr4i 
 |-  ( ( ( ph -> ps ) -> ( ch \/ ( th \/ ta ) ) ) -> ( ( th -> ph ) -> ( ch \/ ( ta \/ ph ) ) ) )
29 4 8 28 syl2im 
 |-  ( ( ( -. ph \/ ps ) -> ( ch \/ ( th \/ ta ) ) ) -> ( ( -. th \/ ph ) -> ( ch \/ ( ta \/ ph ) ) ) )
30 imor 
 |-  ( ( ( -. ph \/ ps ) -> ( ch \/ ( th \/ ta ) ) ) <-> ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) )
31 imor 
 |-  ( ( ( -. th \/ ph ) -> ( ch \/ ( ta \/ ph ) ) ) <-> ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
32 29 30 31 3imtr3i 
 |-  ( ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) -> ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
33 32 imori 
 |-  ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )