Metamath Proof Explorer


Theorem merco2

Description: A single axiom for propositional calculus discovered by C. A. Meredith.

This axiom has 19 symbols, sans auxiliaries. See notes in merco1 . (Contributed by Anthony Hart, 7-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion merco2 ( ( ( 𝜑𝜓 ) → ( ( ⊥ → 𝜒 ) → 𝜃 ) ) → ( ( 𝜃𝜑 ) → ( 𝜏 → ( 𝜂𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 falim ( ⊥ → 𝜒 )
2 pm2.04 ( ( ( 𝜑𝜓 ) → ( ( ⊥ → 𝜒 ) → 𝜃 ) ) → ( ( ⊥ → 𝜒 ) → ( ( 𝜑𝜓 ) → 𝜃 ) ) )
3 1 2 mpi ( ( ( 𝜑𝜓 ) → ( ( ⊥ → 𝜒 ) → 𝜃 ) ) → ( ( 𝜑𝜓 ) → 𝜃 ) )
4 jarl ( ( ( 𝜑𝜓 ) → 𝜃 ) → ( ¬ 𝜑𝜃 ) )
5 idd ( ( ( 𝜑𝜓 ) → 𝜃 ) → ( 𝜃𝜃 ) )
6 4 5 jad ( ( ( 𝜑𝜓 ) → 𝜃 ) → ( ( 𝜑𝜃 ) → 𝜃 ) )
7 looinv ( ( ( 𝜑𝜃 ) → 𝜃 ) → ( ( 𝜃𝜑 ) → 𝜑 ) )
8 3 6 7 3syl ( ( ( 𝜑𝜓 ) → ( ( ⊥ → 𝜒 ) → 𝜃 ) ) → ( ( 𝜃𝜑 ) → 𝜑 ) )
9 8 a1dd ( ( ( 𝜑𝜓 ) → ( ( ⊥ → 𝜒 ) → 𝜃 ) ) → ( ( 𝜃𝜑 ) → ( 𝜏𝜑 ) ) )
10 9 a1i ( 𝜂 → ( ( ( 𝜑𝜓 ) → ( ( ⊥ → 𝜒 ) → 𝜃 ) ) → ( ( 𝜃𝜑 ) → ( 𝜏𝜑 ) ) ) )
11 10 com4l ( ( ( 𝜑𝜓 ) → ( ( ⊥ → 𝜒 ) → 𝜃 ) ) → ( ( 𝜃𝜑 ) → ( 𝜏 → ( 𝜂𝜑 ) ) ) )