Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  re2luk2 Structured version   Unicode version

Theorem re2luk2 1540
 Description: luk-2 1430 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 1529 . . . 4
2 rb-ax3 1528 . . . . . . 7
31, 2rbsyl 1530 . . . . . 6
4 rb-ax4 1529 . . . . . . . . 9
5 rb-ax3 1528 . . . . . . . . 9
64, 5rbsyl 1530 . . . . . . . 8
7 rb-ax2 1527 . . . . . . . 8
86, 7anmp 1525 . . . . . . 7
98, 3rblem1 1531 . . . . . 6
103, 9anmp 1525 . . . . 5
1110, 3rblem1 1531 . . . 4
121, 11rbsyl 1530 . . 3
13 rb-imdf 1524 . . . 4
1413rblem6 1536 . . 3
1512, 14rbsyl 1530 . 2
16 rb-imdf 1524 . . 3
1716rblem7 1537 . 2
1815, 17anmp 1525 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wo 358 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 178  df-or 360  df-an 361
 Copyright terms: Public domain W3C validator