MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE 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  |-  ( ph  <->  ps )
Assertion
Ref Expression
bibi2i  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )

Proof of Theorem bibi2i
StepHypRef Expression
1 id 19 . . 3  |-  ( ( ch  <->  ph )  ->  ( ch 
<-> 
ph ) )
2 bibi.a . . 3  |-  ( ph  <->  ps )
31, 2syl6bb 252 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 19 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2syl6bbr 254 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 180 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bibi1i  305  bibi12i  306  bibi2d  309  con2bi  318  pm4.71r  612  xorass  1299  sblbis  2025  sbrbif  2027  abeq2  2401  abid2f  2457  pm13.183  2921  disj3  3512  euabsn2  3711  axrep5  4152  axsep  4156  ax9vsep  4161  inex1  4171  axpr  4229  zfpair2  4231  sucel  4481  ballotlemfc0  23067  ballotlemfcc  23068  or3dir  23140  abeq2f  23145  rabid2f  23151  totprobd  23644  axrepprim  24063  symdifass  24442  brtxpsd3  24507  bisym1  24930  bnj89  29063  bnj145  29071  sblbisNEW7  29612  sbrbifNEW7  29614
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 177
  Copyright terms: Public domain W3C validator