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

Theorem bibi2i 304
 Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
Hypothesis
Ref Expression
bibi.a
Assertion
Ref Expression
bibi2i

Proof of Theorem bibi2i
StepHypRef Expression
1 id 19 . . 3
2 bibi.a . . 3
31, 2syl6bb 252 . 2
4 id 19 . . 3
54, 2syl6bbr 254 . 2
63, 5impbii 180 1
 Colors of variables: wff setvar class Syntax hints:   wb 176 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 This theorem is referenced by:  bibi1i  305  bibi12i  306  bibi2d  309  con2bi  318  pm4.71r  612  xorass  1308  sblbis  2072  sbrbif  2074  abeq2  2458  abid2f  2514  pm13.183  2979  dfss2  3262  necompl  3544  disj3  3595  euabsn2  3791  axprimlem1  4088  axprimlem2  4089  axxpprim  4090  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  ninexg  4097  1cex  4142  eqpw1  4162  xpkvexg  4285  p6exg  4290  eqop  4611
 Copyright terms: Public domain W3C validator