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

Theorem bibi2i 315
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 265 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 22 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2syl6bbr 267 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 191 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188
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 189
This theorem is referenced by:  bibi1i  316  bibi12i  317  bibi2d  320  con2bi  330  pm4.71r  637  xorass  1409  xorassOLD  1410  sblbis  2233  sbrbif  2235  abeq2  2560  abeq2f  2619  pm13.183  3179  symdifass  3672  disj3  3809  euabsn2  4043  axrep5  4520  axsep  4524  ax6vsep  4529  inex1  4544  axpr  4638  zfpair2  4640  sucel  5496  suppvalbr  6918  bnj89  29527  bnj145OLD  29535  axrepprim  30329  brtxpsd3  30663  bisym1  31079  bj-abeq2  31388  bj-axrep5  31407  bj-axsep  31408  bj-snsetex  31557  ifpidg  36135  nanorxor  36653
  Copyright terms: Public domain W3C validator