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  1354  sblbis  2096  sbrbif  2098  abeq2  2547  abid2f  2603  pm13.183  3099  disj3  3722  euabsn2  3945  axrep5  4407  axsep  4411  ax6vsep  4416  inex1  4432  axpr  4529  zfpair2  4531  sucel  4791  fnsnb  5897  suppvalbr  6693  legtrid  23021  abeq2f  25882  axrepprim  27352  symdifass  27857  brtxpsd3  27926  bisym1  28264  impor  28879  bnj89  31708  bnj145OLD  31716  bj-abeq2  32292  bj-axrep5  32311  bj-axsep  32312  bj-snsetex  32454
  Copyright terms: Public domain W3C validator