MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi2i 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  1314  sblbis  2121  sbrbif  2123  abeq2  2509  abid2f  2565  pm13.183  3036  disj3  3632  euabsn2  3835  axrep5  4285  axsep  4289  ax9vsep  4294  inex1  4304  axpr  4362  zfpair2  4364  sucel  4614  abeq2f  23913  axrepprim  25104  symdifass  25585  brtxpsd3  25650  bisym1  26073  bnj89  28792  bnj145  28800  sblbisNEW7  29342  sbrbifNEW7  29344
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