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

Theorem bibi2i 341
 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 290 . 2 ((𝜒𝜑) → (𝜒𝜓))
4 id 22 . . 3 ((𝜒𝜓) → (𝜒𝜓))
54, 2bitr4di 292 . 2 ((𝜒𝜓) → (𝜒𝜑))
63, 5impbii 212 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209 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 210 This theorem is referenced by:  bibi1i  342  bibi12i  343  bibi2d  346  con2bi  357  pm4.71r  562  xorass  1507  sblbis  2314  sbrbif  2316  sblbisvOLD  2321  sblbisALT  2588  abeq2  2922  abeq2f  2985  pm13.183  3606  dfss2  3901  disj  4355  disj3  4361  axrep5  5160  axrep6  5161  axsepgfromrep  5165  ax6vsep  5171  inex1  5185  axprALT  5288  zfpair2  5296  sucel  6232  suppvalbr  7819  bnj89  32113  axrepprim  33053  brtxpsd3  33482  bisym1  33892  bj-bixor  34054  eliminable-veqab  34320  bj-snsetex  34415  bj-reabeq  34479  wl-3xorbi  34906  sn-axrep5v  39416  ifpidg  40214  nanorxor  41024
 Copyright terms: Public domain W3C validator