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  2012  sbrbif  2014  abeq2  2388  abid2f  2444  pm13.183  2908  disj3  3499  euabsn2  3698  axrep5  4136  axsep  4140  ax9vsep  4145  inex1  4155  axpr  4213  zfpair2  4215  sucel  4465  ballotlemfc0  23051  ballotlemfcc  23052  or3dir  23124  abeq2f  23129  rabid2f  23135  totprobd  23629  axrepprim  24048  symdifass  24371  brtxpsd3  24436  bisym1  24858  bnj89  28747  bnj145  28755
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