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

Theorem bibi2i 313
Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
Hypothesis
Ref Expression
bibi2i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
bibi2i  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )

Proof of Theorem bibi2i
StepHypRef Expression
1 id 22 . . 3  |-  ( ( ch  <->  ph )  ->  ( ch 
<-> 
ph ) )
2 bibi2i.1 . . 3  |-  ( ph  <->  ps )
31, 2syl6bb 261 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 22 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2syl6bbr 263 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 188 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  bibi1i  314  bibi12i  315  bibi2d  318  con2bi  328  pm4.71r  631  xorass  1367  sblbis  2146  sbrbif  2148  abeq2  2581  abid2fOLD  2649  pm13.183  3240  symdifass  3734  disj3  3874  euabsn2  4103  axrep5  4573  axsep  4577  ax6vsep  4582  inex1  4597  axpr  4694  zfpair2  4696  sucel  4960  suppvalbr  6921  abeq2f  27524  axrepprim  29249  brtxpsd3  29708  bisym1  30046  nanorxor  31347  bnj89  33875  bnj145OLD  33883  bj-abeq2  34460  bj-axrep5  34479  bj-axsep  34480  bj-snsetex  34622  bj-ifidg  37808
  Copyright terms: Public domain W3C validator