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

Proof of Theorem bibi2i
StepHypRef Expression
1 id 19 . . 3 ((𝜒𝜑) → (𝜒𝜑))
2 bibi.a . . 3 (𝜑𝜓)
31, 2syl6bb 195 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 19 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2syl6bbr 197 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 125 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 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  387  sblbis  1933  sbrbif  1935  abeq2  2248  abid2f  2306  necon4biddc  2383  pm13.183  2822  disj3  3415  euabsn2  3592  a9evsep  4050  inex1  4062  zfpair2  4132  sucel  4332  bdinex1  13150  bj-zfpair2  13161  bj-d0clsepcl  13176
 Copyright terms: Public domain W3C validator