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

Theorem bibi2i 328
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 278 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 22 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2syl6bbr 280 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 200 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  bibi1i  329  bibi12i  330  bibi2d  333  con2bi  344  pm4.71r  550  xorass  1622  sblbis  2565  sbrbif  2567  abeq2  2915  abeq2f  2975  pm13.183  3538  symdifassOLD  4049  disj3  4215  euabsn2  4448  axrep5  4966  axsep  4970  ax6vsep  4975  inex1  4991  axpr  5092  zfpair2  5094  sucel  6008  suppvalbr  7530  bnj89  31109  axrepprim  31898  brtxpsd3  32321  bisym1  32732  bj-abeq2  33084  bj-axrep5  33103  bj-axsep  33104  bj-snsetex  33258  ifpidg  38333  nanorxor  39001
  Copyright terms: Public domain W3C validator