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

Theorem bibi2i 220
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 189 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 19 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2syl6bbr 191 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 121 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bibi1i  221  bibi12i  222  bibi2d  225  pm4.71r  376  sblbis  1850  sbrbif  1852  abeq2  2162  abid2f  2218  necon4biddc  2295  pm13.183  2704  disj3  3300  euabsn2  3467  a9evsep  3907  inex1  3919  zfpair2  3973  sucel  4175  bdinex1  10406  bj-zfpair2  10417  bj-d0clsepcl  10436
  Copyright terms: Public domain W3C validator