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 275 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 22 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2syl6bbr 277 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 198 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  bibi1i  327  bibi12i  328  bibi2d  331  con2bi  342  pm4.71r  661  xorass  1460  sblbis  2392  sbrbif  2394  abeq2  2719  abeq2f  2778  pm13.183  3313  symdifass  3815  disj3  3973  euabsn2  4204  axrep5  4699  axsep  4703  ax6vsep  4708  inex1  4722  axpr  4827  zfpair2  4829  sucel  5701  suppvalbr  7164  bnj89  29835  bnj145OLD  29843  axrepprim  30627  brtxpsd3  30967  bisym1  31382  bj-abeq2  31755  bj-axrep5  31774  bj-axsep  31775  bj-snsetex  31938  ifpidg  36649  nanorxor  37320
  Copyright terms: Public domain W3C validator