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

Theorem re2luk2 1531
Description: luk-2 1421 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
re2luk2 ((¬ φφ) → φ)

Proof of Theorem re2luk2
StepHypRef Expression
1 rb-ax4 1520 . . . 4 (¬ (φ φ) φ)
2 rb-ax3 1519 . . . . . . 7 φ (φ φ))
31, 2rbsyl 1521 . . . . . 6 φ φ)
4 rb-ax4 1520 . . . . . . . . 9 (¬ (¬ ¬ φ ¬ ¬ φ) ¬ ¬ φ)
5 rb-ax3 1519 . . . . . . . . 9 (¬ ¬ ¬ φ (¬ ¬ φ ¬ ¬ φ))
64, 5rbsyl 1521 . . . . . . . 8 (¬ ¬ ¬ φ ¬ ¬ φ)
7 rb-ax2 1518 . . . . . . . 8 (¬ (¬ ¬ ¬ φ ¬ ¬ φ) (¬ ¬ φ ¬ ¬ ¬ φ))
86, 7anmp 1516 . . . . . . 7 (¬ ¬ φ ¬ ¬ ¬ φ)
98, 3rblem1 1522 . . . . . 6 (¬ (¬ φ φ) (¬ ¬ ¬ φ φ))
103, 9anmp 1516 . . . . 5 (¬ ¬ ¬ φ φ)
1110, 3rblem1 1522 . . . 4 (¬ (¬ ¬ φ φ) (φ φ))
121, 11rbsyl 1521 . . 3 (¬ (¬ ¬ φ φ) φ)
13 rb-imdf 1515 . . . 4 ¬ (¬ (¬ (¬ φφ) (¬ ¬ φ φ)) ¬ (¬ (¬ ¬ φ φ) φφ)))
1413rblem6 1527 . . 3 (¬ (¬ φφ) (¬ ¬ φ φ))
1512, 14rbsyl 1521 . 2 (¬ (¬ φφ) φ)
16 rb-imdf 1515 . . 3 ¬ (¬ (¬ ((¬ φφ) → φ) (¬ (¬ φφ) φ)) ¬ (¬ (¬ (¬ φφ) φ) ((¬ φφ) → φ)))
1716rblem7 1528 . 2 (¬ (¬ (¬ φφ) φ) ((¬ φφ) → φ))
1815, 17anmp 1516 1 ((¬ φφ) → φ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wo 357
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 177  df-or 359  df-an 360
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator