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

Theorem bibi2i 314
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 23 . . 3  |-  ( ( ch  <->  ph )  ->  ( ch 
<-> 
ph ) )
2 bibi2i.1 . . 3  |-  ( ph  <->  ps )
31, 2syl6bb 264 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 23 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2syl6bbr 266 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 190 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  bibi1i  315  bibi12i  316  bibi2d  319  con2bi  329  pm4.71r  635  xorass  1404  xorassOLD  1405  sblbis  2196  sbrbif  2198  abeq2  2544  abid2fOLD  2612  abeq2f  2613  pm13.183  3209  symdifass  3699  disj3  3834  euabsn2  4065  axrep5  4534  axsep  4538  ax6vsep  4543  inex1  4557  axpr  4651  zfpair2  4653  sucel  5506  suppvalbr  6920  bnj89  29312  bnj145OLD  29320  axrepprim  30114  brtxpsd3  30445  bisym1  30861  bj-abeq2  31136  bj-axrep5  31155  bj-axsep  31156  bj-snsetex  31303  ifpidg  35838  nanorxor  36294
  Copyright terms: Public domain W3C validator