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 ( ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) ∨ ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 orc ( ¬ 𝜑 → ( ¬ 𝜑𝜓 ) )
2 olc ( 𝜓 → ( ¬ 𝜑𝜓 ) )
3 1 2 ja ( ( 𝜑𝜓 ) → ( ¬ 𝜑𝜓 ) )
4 3 imim1i ( ( ( ¬ 𝜑𝜓 ) → ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) )
5 pm2.24 ( 𝜃 → ( ¬ 𝜃𝜑 ) )
6 idd ( 𝜃 → ( 𝜑𝜑 ) )
7 5 6 jaod ( 𝜃 → ( ( ¬ 𝜃𝜑 ) → 𝜑 ) )
8 7 com12 ( ( ¬ 𝜃𝜑 ) → ( 𝜃𝜑 ) )
9 pm1.5 ( ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( 𝜒 ∨ ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜃𝜏 ) ) ) )
10 pm2.3 ( ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜃𝜏 ) ) → ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜏𝜃 ) ) )
11 pm1.5 ( ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜏𝜃 ) ) → ( 𝜏 ∨ ( ¬ ( 𝜑𝜓 ) ∨ 𝜃 ) ) )
12 pm2.21 ( ¬ 𝜑 → ( 𝜑𝜓 ) )
13 jcn ( 𝜃 → ( ¬ 𝜑 → ¬ ( 𝜃𝜑 ) ) )
14 12 13 imim12i ( ( ( 𝜑𝜓 ) → 𝜃 ) → ( ¬ 𝜑 → ( ¬ 𝜑 → ¬ ( 𝜃𝜑 ) ) ) )
15 14 pm2.43d ( ( ( 𝜑𝜓 ) → 𝜃 ) → ( ¬ 𝜑 → ¬ ( 𝜃𝜑 ) ) )
16 15 con4d ( ( ( 𝜑𝜓 ) → 𝜃 ) → ( ( 𝜃𝜑 ) → 𝜑 ) )
17 imor ( ( ( 𝜑𝜓 ) → 𝜃 ) ↔ ( ¬ ( 𝜑𝜓 ) ∨ 𝜃 ) )
18 imor ( ( ( 𝜃𝜑 ) → 𝜑 ) ↔ ( ¬ ( 𝜃𝜑 ) ∨ 𝜑 ) )
19 16 17 18 3imtr3i ( ( ¬ ( 𝜑𝜓 ) ∨ 𝜃 ) → ( ¬ ( 𝜃𝜑 ) ∨ 𝜑 ) )
20 19 orim2i ( ( 𝜏 ∨ ( ¬ ( 𝜑𝜓 ) ∨ 𝜃 ) ) → ( 𝜏 ∨ ( ¬ ( 𝜃𝜑 ) ∨ 𝜑 ) ) )
21 pm1.5 ( ( 𝜏 ∨ ( ¬ ( 𝜃𝜑 ) ∨ 𝜑 ) ) → ( ¬ ( 𝜃𝜑 ) ∨ ( 𝜏𝜑 ) ) )
22 10 11 20 21 4syl ( ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜃𝜏 ) ) → ( ¬ ( 𝜃𝜑 ) ∨ ( 𝜏𝜑 ) ) )
23 22 orim2i ( ( 𝜒 ∨ ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜃𝜏 ) ) ) → ( 𝜒 ∨ ( ¬ ( 𝜃𝜑 ) ∨ ( 𝜏𝜑 ) ) ) )
24 pm1.5 ( ( 𝜒 ∨ ( ¬ ( 𝜃𝜑 ) ∨ ( 𝜏𝜑 ) ) ) → ( ¬ ( 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
25 9 23 24 3syl ( ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( ¬ ( 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
26 imor ( ( ( 𝜑𝜓 ) → ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) ↔ ( ¬ ( 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) )
27 imor ( ( ( 𝜃𝜑 ) → ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) ↔ ( ¬ ( 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
28 25 26 27 3imtr4i ( ( ( 𝜑𝜓 ) → ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( ( 𝜃𝜑 ) → ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
29 4 8 28 syl2im ( ( ( ¬ 𝜑𝜓 ) → ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( ( ¬ 𝜃𝜑 ) → ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
30 imor ( ( ( ¬ 𝜑𝜓 ) → ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) ↔ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) )
31 imor ( ( ( ¬ 𝜃𝜑 ) → ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) ↔ ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
32 29 30 31 3imtr3i ( ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
33 32 imori ( ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) ∨ ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )