New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  merco1lem1 GIF version

Theorem merco1lem1 1479
 Description: Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
merco1lem1 (φ → ( ⊥ → χ))

Proof of Theorem merco1lem1
StepHypRef Expression
1 merco1 1478 . . . . 5 ((((( ⊥ → φ) → (φ → ⊥ )) → (φ → ⊥ )) → ( ⊥ → φ)) → ((( ⊥ → φ) → ⊥ ) → (φ → ⊥ )))
2 merco1 1478 . . . . 5 (((((( ⊥ → φ) → (φ → ⊥ )) → (φ → ⊥ )) → ( ⊥ → φ)) → ((( ⊥ → φ) → ⊥ ) → (φ → ⊥ ))) → ((((( ⊥ → φ) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → (φ → ( ⊥ → φ))))
31, 2ax-mp 8 . . . 4 ((((( ⊥ → φ) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → (φ → ( ⊥ → φ)))
4 merco1 1478 . . . 4 (((((( ⊥ → φ) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → (φ → ( ⊥ → φ))) → (((φ → ( ⊥ → φ)) → ( ⊥ → φ)) → (φ → ( ⊥ → φ))))
53, 4ax-mp 8 . . 3 (((φ → ( ⊥ → φ)) → ( ⊥ → φ)) → (φ → ( ⊥ → φ)))
6 merco1 1478 . . . . 5 ((((( ⊥ → φ) → (φ → ⊥ )) → ((φ → ( ⊥ → φ)) → ⊥ )) → (φ → ( ⊥ → φ))) → (((φ → ( ⊥ → φ)) → ⊥ ) → (φ → ⊥ )))
7 merco1 1478 . . . . 5 (((((( ⊥ → φ) → (φ → ⊥ )) → ((φ → ( ⊥ → φ)) → ⊥ )) → (φ → ( ⊥ → φ))) → (((φ → ( ⊥ → φ)) → ⊥ ) → (φ → ⊥ ))) → (((((φ → ( ⊥ → φ)) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → ((φ → ( ⊥ → φ)) → ( ⊥ → φ))))
86, 7ax-mp 8 . . . 4 (((((φ → ( ⊥ → φ)) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → ((φ → ( ⊥ → φ)) → ( ⊥ → φ)))
9 merco1 1478 . . . 4 ((((((φ → ( ⊥ → φ)) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → ((φ → ( ⊥ → φ)) → ( ⊥ → φ))) → ((((φ → ( ⊥ → φ)) → ( ⊥ → φ)) → (φ → ( ⊥ → φ))) → (φ → (φ → ( ⊥ → φ)))))
108, 9ax-mp 8 . . 3 ((((φ → ( ⊥ → φ)) → ( ⊥ → φ)) → (φ → ( ⊥ → φ))) → (φ → (φ → ( ⊥ → φ))))
115, 10ax-mp 8 . 2 (φ → (φ → ( ⊥ → φ)))
12 merco1 1478 . . . . 5 ((((( ⊥ → φ) → (φ → ⊥ )) → (φ → ⊥ )) → ( ⊥ → χ)) → ((( ⊥ → χ) → ⊥ ) → (φ → ⊥ )))
13 merco1 1478 . . . . 5 (((((( ⊥ → φ) → (φ → ⊥ )) → (φ → ⊥ )) → ( ⊥ → χ)) → ((( ⊥ → χ) → ⊥ ) → (φ → ⊥ ))) → ((((( ⊥ → χ) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → (φ → ( ⊥ → φ))))
1412, 13ax-mp 8 . . . 4 ((((( ⊥ → χ) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → (φ → ( ⊥ → φ)))
15 merco1 1478 . . . 4 (((((( ⊥ → χ) → ⊥ ) → (φ → ⊥ )) → ( ⊥ → φ)) → (φ → ( ⊥ → φ))) → (((φ → ( ⊥ → φ)) → ( ⊥ → χ)) → (φ → ( ⊥ → χ))))
1614, 15ax-mp 8 . . 3 (((φ → ( ⊥ → φ)) → ( ⊥ → χ)) → (φ → ( ⊥ → χ)))
17 merco1 1478 . . . . 5 ((((( ⊥ → χ) → ((φ → (φ → ( ⊥ → φ))) → ⊥ )) → ((φ → ( ⊥ → φ)) → ⊥ )) → (φ → ( ⊥ → χ))) → (((φ → ( ⊥ → χ)) → ⊥ ) → ((φ → (φ → ( ⊥ → φ))) → ⊥ )))
18 merco1 1478 . . . . 5 (((((( ⊥ → χ) → ((φ → (φ → ( ⊥ → φ))) → ⊥ )) → ((φ → ( ⊥ → φ)) → ⊥ )) → (φ → ( ⊥ → χ))) → (((φ → ( ⊥ → χ)) → ⊥ ) → ((φ → (φ → ( ⊥ → φ))) → ⊥ ))) → (((((φ → ( ⊥ → χ)) → ⊥ ) → ((φ → (φ → ( ⊥ → φ))) → ⊥ )) → ( ⊥ → χ)) → ((φ → ( ⊥ → φ)) → ( ⊥ → χ))))
1917, 18ax-mp 8 . . . 4 (((((φ → ( ⊥ → χ)) → ⊥ ) → ((φ → (φ → ( ⊥ → φ))) → ⊥ )) → ( ⊥ → χ)) → ((φ → ( ⊥ → φ)) → ( ⊥ → χ)))
20 merco1 1478 . . . 4 ((((((φ → ( ⊥ → χ)) → ⊥ ) → ((φ → (φ → ( ⊥ → φ))) → ⊥ )) → ( ⊥ → χ)) → ((φ → ( ⊥ → φ)) → ( ⊥ → χ))) → ((((φ → ( ⊥ → φ)) → ( ⊥ → χ)) → (φ → ( ⊥ → χ))) → ((φ → (φ → ( ⊥ → φ))) → (φ → ( ⊥ → χ)))))
2119, 20ax-mp 8 . . 3 ((((φ → ( ⊥ → φ)) → ( ⊥ → χ)) → (φ → ( ⊥ → χ))) → ((φ → (φ → ( ⊥ → φ))) → (φ → ( ⊥ → χ))))
2216, 21ax-mp 8 . 2 ((φ → (φ → ( ⊥ → φ))) → (φ → ( ⊥ → χ)))
2311, 22ax-mp 8 1 (φ → ( ⊥ → χ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊥ wfal 1317 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-tru 1319  df-fal 1320 This theorem is referenced by:  retbwax4  1480  retbwax2  1481
 Copyright terms: Public domain W3C validator