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

Proof

Step Hyp Ref Expression
1 meran1 ( ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) ∨ ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
2 1 imorri ( ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) )
3 meran1 ( ¬ ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) ∨ ( ¬ ( ¬ 𝜏𝜃 ) ∨ ( 𝜒 ∨ ( 𝜑𝜃 ) ) ) )
4 3 imorri ( ( ¬ ( ¬ 𝜃𝜑 ) ∨ ( 𝜒 ∨ ( 𝜏𝜑 ) ) ) → ( ¬ ( ¬ 𝜏𝜃 ) ∨ ( 𝜒 ∨ ( 𝜑𝜃 ) ) ) )
5 2 4 syl ( ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) → ( ¬ ( ¬ 𝜏𝜃 ) ∨ ( 𝜒 ∨ ( 𝜑𝜃 ) ) ) )
6 5 imori ( ¬ ( ¬ ( ¬ 𝜑𝜓 ) ∨ ( 𝜒 ∨ ( 𝜃𝜏 ) ) ) ∨ ( ¬ ( ¬ 𝜏𝜃 ) ∨ ( 𝜒 ∨ ( 𝜑𝜃 ) ) ) )