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

Theorem bibi2i 226
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, 2bitrdi 195 . 2  |-  ( ( ch  <->  ph )  ->  ( ch 
<->  ps ) )
4 id 19 . . 3  |-  ( ( ch  <->  ps )  ->  ( ch 
<->  ps ) )
54, 2bitr4di 197 . 2  |-  ( ( ch  <->  ps )  ->  ( ch 
<-> 
ph ) )
63, 5impbii 125 1  |-  ( ( ch  <->  ph )  <->  ( ch  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bibi1i  227  bibi12i  228  bibi2d  231  pm4.71r  388  sblbis  1953  sbrbif  1955  abeq2  2279  abid2f  2338  necon4biddc  2415  pm13.183  2868  disj3  3466  euabsn2  3650  a9evsep  4109  inex1  4121  zfpair2  4193  sucel  4393  bdinex1  13894  bj-zfpair2  13905  bj-d0clsepcl  13920
  Copyright terms: Public domain W3C validator