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

Theorem bibi2i 326
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  327  bibi12i  328  bibi2d  331  con2bi  342  pm4.71r  666  xorass  1617  sblbis  2542  sbrbif  2544  abeq2  2871  abeq2f  2931  pm13.183  3485  symdifass  3997  disj3  4165  euabsn2  4405  axrep5  4929  axsep  4933  ax6vsep  4938  inex1  4952  axpr  5055  zfpair2  5057  sucel  5960  suppvalbr  7469  bnj89  31118  axrepprim  31908  brtxpsd3  32331  bisym1  32746  bj-abeq2  33102  bj-axrep5  33121  bj-axsep  33122  bj-snsetex  33276  ifpidg  38357  nanorxor  39025
  Copyright terms: Public domain W3C validator