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

Theorem bibi2i 320
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 269 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 22 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2syl6bbr 271 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 192 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189
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 190
This theorem is referenced by:  bibi1i  321  bibi12i  322  bibi2d  325  con2bi  335  pm4.71r  643  xorass  1434  xorassOLD  1435  sblbis  2253  sbrbif  2255  abeq2  2580  abeq2f  2639  pm13.183  3167  symdifass  3663  disj3  3813  euabsn2  4034  axrep5  4513  axsep  4517  ax6vsep  4522  inex1  4537  axpr  4638  zfpair2  4640  sucel  5503  suppvalbr  6937  bnj89  29599  bnj145OLD  29607  axrepprim  30401  brtxpsd3  30734  bisym1  31150  bj-abeq2  31454  bj-axrep5  31473  bj-axsep  31474  bj-snsetex  31627  ifpidg  36206  nanorxor  36723
  Copyright terms: Public domain W3C validator