Metamath Proof Explorer


Theorem retbwax1

Description: tbw-ax1 rederived from merco1 .

This theorem, along with retbwax2 , retbwax3 , and retbwax4 , shows that merco1 with ax-mp can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 18-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion retbwax1 ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 merco1lem18 ( ( 𝜓 → ( 𝜑𝜒 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) )
2 merco1lem16 ( ( ( 𝜓 → ( 𝜑𝜒 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) )
3 1 2 ax-mp ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) )
4 merco1lem15 ( ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) )
5 merco1lem15 ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) )
6 4 5 ax-mp ( ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) )
7 merco1lem18 ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) )
8 6 7 ax-mp ( ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) )
9 merco1lem14 ( ( ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) )
10 8 9 ax-mp ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) )
11 merco1lem14 ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( 𝜑𝜒 ) ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) )
12 merco1lem10 ( ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) → ⊥ ) → ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ⊥ ) ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) ) → ( ( ( 𝜑𝜒 ) → 𝜑 ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) ) )
13 merco1 ( ( ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) → ⊥ ) → ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ⊥ ) ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) ) → ( ( ( 𝜑𝜒 ) → 𝜑 ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) ) ) → ( ( ( ( ( 𝜑𝜒 ) → 𝜑 ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) → ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) ) )
14 12 13 ax-mp ( ( ( ( ( 𝜑𝜒 ) → 𝜑 ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) → ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) )
15 merco1 ( ( ( ( ( ( 𝜑𝜒 ) → 𝜑 ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) → ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) ) → ( ( ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) → ( 𝜑𝜒 ) ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( 𝜑𝜒 ) ) ) )
16 14 15 ax-mp ( ( ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) → ( 𝜑𝜒 ) ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( 𝜑𝜒 ) ) )
17 merco1 ( ( ( ( ( ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) → 𝜑 ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ⊥ ) ) → ( 𝜑𝜒 ) ) → ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( 𝜑𝜒 ) ) ) → ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( 𝜑𝜒 ) ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) )
18 16 17 ax-mp ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( 𝜑𝜒 ) ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) )
19 11 18 ax-mp ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) )
20 merco1lem15 ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) → ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) )
21 19 20 ax-mp ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) )
22 merco1lem10 ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) )
23 merco1lem9 ( ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) ) → ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) )
24 22 23 ax-mp ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) )
25 merco1lem13 ( ( ( ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) → ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) ) )
26 24 25 ax-mp ( ( ( ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ⊥ ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) )
27 21 26 ax-mp ( ( ( 𝜓𝜒 ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) ) → ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) ) )
28 10 27 ax-mp ( ( ( 𝜓𝜒 ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) ) )
29 3 28 ax-mp ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) )