ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bibi2i GIF 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 (𝜑𝜓)
Assertion
Ref Expression
bibi2i ((𝜒𝜑) ↔ (𝜒𝜓))

Proof of Theorem bibi2i
StepHypRef Expression
1 id 19 . . 3 ((𝜒𝜑) → (𝜒𝜑))
2 bibi.a . . 3 (𝜑𝜓)
31, 2syl6bb 194 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 19 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2syl6bbr 196 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 124 1 ((𝜒𝜑) ↔ (𝜒𝜓))
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  1882  sbrbif  1884  abeq2  2196  abid2f  2253  necon4biddc  2330  pm13.183  2754  disj3  3335  euabsn2  3511  a9evsep  3961  inex1  3973  zfpair2  4037  sucel  4237  bdinex1  11790  bj-zfpair2  11801  bj-d0clsepcl  11820
  Copyright terms: Public domain W3C validator