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

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

Proof of Theorem bibi2i
StepHypRef Expression
1 id 22 . . 3
2 bibi2i.1 . . 3
31, 2syl6bb 261 . 2
4 id 22 . . 3
54, 2syl6bbr 263 . 2
63, 5impbii 188 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184 This theorem is referenced by:  bibi1i  314  bibi12i  315  bibi2d  318  con2bi  328  pm4.71r  631  xorass  1367  sblbis  2145  sbrbif  2147  abeq2  2581  abid2fOLD  2649  pm13.183  3240  disj3  3871  euabsn2  4101  axrep5  4568  axsep  4572  ax6vsep  4577  inex1  4593  axpr  4690  zfpair2  4692  sucel  4956  suppvalbr  6922  abeq2f  27398  axrepprim  29074  symdifass  29477  brtxpsd3  29546  bisym1  29884  nanorxor  31185  bnj89  33774  bnj145OLD  33782  bj-abeq2  34359  bj-axrep5  34378  bj-axsep  34379  bj-snsetex  34521  bj-ifidg  37707 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 185
 Copyright terms: Public domain W3C validator