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

Theorem hbimdOLD 1816
Description: Obsolete proof of hbimd 1815 as of 16-Dec-2017. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.)
Hypotheses
Ref Expression
hbimd.1
hbimd.2
hbimd.3
Assertion
Ref Expression
hbimdOLD

Proof of Theorem hbimdOLD
StepHypRef Expression
1 hbimd.1 . . . . 5
2 hbimd.2 . . . . 5
31, 2alrimih 1565 . . . 4
4 sp 1747 . . . . . 6
5 hbn1 1730 . . . . . 6
64, 5nsyl4 134 . . . . 5
76con1i 121 . . . 4
8 con3 126 . . . . 5
98al2imi 1561 . . . 4
103, 7, 9syl2im 34 . . 3
11 pm2.21 100 . . . 4
1211alimi 1559 . . 3
1310, 12syl6 29 . 2
14 hbimd.3 . . 3
15 ax-1 5 . . . 4
1615alimi 1559 . . 3
1714, 16syl6 29 . 2
1813, 17jad 154 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator