Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi2i Structured version   Visualization version   GIF version

Theorem bibi2i 327
 Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
Hypothesis
Ref Expression
bibi2i.1 (𝜑𝜓)
Assertion
Ref Expression
bibi2i ((𝜒𝜑) ↔ (𝜒𝜓))

Proof of Theorem bibi2i
StepHypRef Expression
1 id 22 . . 3 ((𝜒𝜑) → (𝜒𝜑))
2 bibi2i.1 . . 3 (𝜑𝜓)
31, 2syl6bb 276 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 22 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2syl6bbr 278 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 199 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197 This theorem is referenced by:  bibi1i  328  bibi12i  329  bibi2d  332  con2bi  343  pm4.71r  662  xorass  1465  sblbis  2403  sbrbif  2405  abeq2  2729  abeq2f  2788  pm13.183  3332  symdifass  3837  disj3  3999  euabsn2  4237  axrep5  4746  axsep  4750  ax6vsep  4755  inex1  4769  axpr  4876  zfpair2  4878  sucel  5767  suppvalbr  7259  bnj89  30548  bnj145OLD  30556  axrepprim  31340  brtxpsd3  31698  bisym1  32113  bj-abeq2  32469  bj-axrep5  32488  bj-axsep  32489  bj-snsetex  32651  ifpidg  37356  nanorxor  38025
 Copyright terms: Public domain W3C validator