Theorem imbi2i 226

Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)

Hypothesis

Ref	Expression
bi.a	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi2i	⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		bi.a	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 180	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12i  239  anidmdbi  398  nan  696  sbcof2  1856  sblimv  1941  sbhb  1991  sblim  2008  2sb6  2035  sbcom2v  2036  2sb6rf  2041  eu1  2102  moabs  2127  mo3h  2131  moanim  2152  2moswapdc  2168  r2alf  2547  r19.21t  2605  rspc2gv  2920  reu2  2992  reu8  3000  2reuswapdc  3008  2rmorex  3010  dfdif3  3315  ssconb  3338  ssin  3427  reldisj  3544  ssundifim  3576  ralm  3596  unissb  3919  repizf2lem  4247  elirr  4635  en2lp  4648  tfi  4676  ssrel  4810  ssrel2  4812  fncnv  5391  fun11  5392  axcaucvglemres  8107  axpre-suploc  8110  suprzclex  9566  raluz2  9801  supinfneg  9817  infsupneg  9818  infssuzex  10481  bezoutlemmain  12556  isprm2  12676  lmres  14959  ivthdich  15364  limcdifap  15373