ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bibi2i Unicode version

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

Proof of Theorem bibi2i
StepHypRef Expression
1 id 19 . . 3  |-  ( ( ch  <->  ph )  ->  ( ch 
<-> 
ph ) )
2 bibi.a . . 3  |-  ( ph  <->  ps )
31, 2syl6bb 194 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 19 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2syl6bbr 196 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 124 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bibi1i  226  bibi12i  227  bibi2d  230  pm4.71r  382  sblbis  1879  sbrbif  1881  abeq2  2193  abid2f  2249  necon4biddc  2326  pm13.183  2745  disj3  3323  euabsn2  3493  a9evsep  3934  inex1  3946  zfpair2  4009  sucel  4209  bdinex1  11219  bj-zfpair2  11230  bj-d0clsepcl  11249
  Copyright terms: Public domain W3C validator