MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  merco1lem17 Structured version   Visualization version   Unicode version
Theorem merco1lem17 1658
Description: Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
merco1lem17 |- ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ta ) -> ( ( ph -> ch ) -> ta ) )
Proof of Theorem merco1lem17
StepHypRef Expression
1 merco1lem11 1652 . . . . . 6 |- ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) )
2 merco1lem7 1647 . . . . . . . 8 |- ( ( ( ( ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) -> ph ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> F. ) ) -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
3 merco1 1638 . . . . . . . 8 |- ( ( ( ( ( ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) -> ph ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> F. ) ) -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) ) )
42, 3ax-mp 5 . . . . . . 7 |- ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) )
5 merco1lem9 1650 . . . . . . 7 |- ( ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) )
64, 5ax-mp 5 . . . . . 6 |- ( ( ( ( ( ph -> ps ) -> ph ) -> ph ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) ) -> ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) )
71, 6ax-mp 5 . . . . 5 |- ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph )
8 merco1 1638 . . . . 5 |- ( ( ( ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ph ) -> F. ) ) -> F. ) -> ph ) -> ( ( ph -> ch ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) )
97, 8ax-mp 5 . . . 4 |- ( ( ph -> ch ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) )
10 merco1lem11 1652 . . . . . 6 |- ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) )
11 merco1lem7 1647 . . . . . . . 8 |- ( ( ( ( ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) -> ph ) -> ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> F. ) ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) )
12 merco1 1638 . . . . . . . 8 |- ( ( ( ( ( ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) -> ph ) -> ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> F. ) ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) ) )
1311, 12ax-mp 5 . . . . . . 7 |- ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) )
14 merco1lem9 1650 . . . . . . 7 |- ( ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) ) -> ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) )
1513, 14ax-mp 5 . . . . . 6 |- ( ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ph -> ch ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) ) -> ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) )
1610, 15ax-mp 5 . . . . 5 |- ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) )
17 merco1 1638 . . . . 5 |- ( ( ( ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ph ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> F. ) ) -> F. ) -> ( ph -> ch ) ) -> ( ( ( ph -> ch ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) ) )
1816, 17ax-mp 5 . . . 4 |- ( ( ( ph -> ch ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) -> ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) )
199, 18ax-mp 5 . . 3 |- ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) )
20 merco1lem4 1644 . . 3 |- ( ( ( ( ta -> ph ) -> ( ( ph -> ch ) -> F. ) ) -> ch ) -> ( ( ( ph -> ch ) -> F. ) -> ch ) )
21 merco1lem16 1657 . . 3 |- ( ( ( ( ( ph -> ch ) -> F. ) -> ( ph -> ch ) ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) -> ( ( ( ( ph -> ch ) -> F. ) -> ch ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) )
2219, 20, 21mpsyl 68 . 2 |- ( ( ( ( ta -> ph ) -> ( ( ph -> ch ) -> F. ) ) -> ch ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) )
23 merco1 1638 . 2 |- ( ( ( ( ( ta -> ph ) -> ( ( ph -> ch ) -> F. ) ) -> ch ) -> ( ( ( ph -> ps ) -> ph ) -> ch ) ) -> ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ta ) -> ( ( ph -> ch ) -> ta ) ) )
2422, 23ax-mp 5 1 |- ( ( ( ( ( ph -> ps ) -> ph ) -> ch ) -> ta ) -> ( ( ph -> ch ) -> ta ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   F. wfal 1488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-tru 1486  df-fal 1489
This theorem is referenced by:  merco1lem18  1659
  Copyright terms: Public domain W3C validator