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  2107  sbrbif  2109  abeq2  2494  abid2f  2550  pm13.183  3021  disj3  3617  euabsn2  3820  axrep5  4268  axsep  4272  ax9vsep  4277  inex1  4287  axpr  4345  zfpair2  4347  sucel  4597  abeq2f  23806  axrepprim  24932  symdifass  25397  brtxpsd3  25462  bisym1  25885  bnj89  28426  bnj145  28434  sblbisNEW7  28976  sbrbifNEW7  28978
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