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

Theorem tbwlem2 1471
 Description: Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
tbwlem2 ((φ → (ψ → ⊥ )) → (((φχ) → θ) → (ψθ)))

Proof of Theorem tbwlem2
StepHypRef Expression
1 tbw-ax4 1468 . . . . 5 ( ⊥ → χ)
2 tbw-ax1 1465 . . . . . 6 ((ψ → ⊥ ) → (( ⊥ → χ) → (ψχ)))
3 tbwlem1 1470 . . . . . 6 (((ψ → ⊥ ) → (( ⊥ → χ) → (ψχ))) → (( ⊥ → χ) → ((ψ → ⊥ ) → (ψχ))))
42, 3ax-mp 8 . . . . 5 (( ⊥ → χ) → ((ψ → ⊥ ) → (ψχ)))
51, 4ax-mp 8 . . . 4 ((ψ → ⊥ ) → (ψχ))
6 tbwlem1 1470 . . . 4 (((ψ → ⊥ ) → (ψχ)) → (ψ → ((ψ → ⊥ ) → χ)))
75, 6ax-mp 8 . . 3 (ψ → ((ψ → ⊥ ) → χ))
8 tbw-ax1 1465 . . 3 ((φ → (ψ → ⊥ )) → (((ψ → ⊥ ) → χ) → (φχ)))
9 tbw-ax1 1465 . . 3 ((ψ → ((ψ → ⊥ ) → χ)) → ((((ψ → ⊥ ) → χ) → (φχ)) → (ψ → (φχ))))
107, 8, 9mpsyl 59 . 2 ((φ → (ψ → ⊥ )) → (ψ → (φχ)))
11 tbw-ax1 1465 . 2 ((ψ → (φχ)) → (((φχ) → θ) → (ψθ)))
1210, 11tbwsyl 1469 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:  tbwlem4  1473
 Copyright terms: Public domain W3C validator