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

Theorem bibi2i 305
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 20 . . 3  |-  ( ( ch  <->  ph )  ->  ( ch 
<-> 
ph ) )
2 bibi.a . . 3  |-  ( ph  <->  ps )
31, 2syl6bb 253 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 20 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2syl6bbr 255 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 181 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bibi1i  306  bibi12i  307  bibi2d  310  con2bi  319  pm4.71r  613  xorass  1317  sblbis  2146  sbrbif  2148  abeq2  2540  abid2f  2596  pm13.183  3068  disj3  3664  euabsn2  3867  axrep5  4317  axsep  4321  ax9vsep  4326  inex1  4336  axpr  4394  zfpair2  4396  sucel  4646  abeq2f  23952  axrepprim  25143  symdifass  25664  brtxpsd3  25733  bisym1  26161  bnj89  29023  bnj145  29031  sblbisNEW7  29578  sbrbifNEW7  29580
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 178
  Copyright terms: Public domain W3C validator