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  1615  sblbis  2539  sbrbif  2541  abeq2  2868  abeq2f  2928  pm13.183  3482  symdifass  3994  disj3  4162  euabsn2  4402  axrep5  4926  axsep  4930  ax6vsep  4935  inex1  4949  axpr  5052  zfpair2  5054  sucel  5957  suppvalbr  7465  bnj89  31094  axrepprim  31884  brtxpsd3  32307  bisym1  32722  bj-abeq2  33077  bj-axrep5  33096  bj-axsep  33097  bj-snsetex  33255  ifpidg  38336  nanorxor  39004
  Copyright terms: Public domain W3C validator