Theorem imbi2i 303

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 10	. 2 ⊢ (χ → (φ ↔ ψ))
3	2	pm5.74i 236	1 ⊢ ((χ → φ) ↔ (χ → ψ))

Syntax hints:   → wi 4   ↔ wb 176

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 177

This theorem is referenced by:  imbi12i  316  iman  413  pm4.14  561  nan  563  pm5.32  617  anidmdbi  627  imimorb  847  pm5.6  878  exp3acom23g  1371  19.36  1871  sblim  2068  sban  2069  sbhb  2107  2sb6  2113  2sb6rf  2118  eu1  2225  moabs  2248  moanim  2260  2eu6  2289  axi12  2333  r2alf  2649  r19.21t  2699  r19.35  2758  reu2  3024  reu8  3032  2reu5lem3  3043  ssconb  3399  ssin  3477  difin  3492  reldisj  3594  ssundif  3633  pwpw0  3855  pwsnALT  3882  unissb  3921  evenodddisj  4516  tfinnn  4534  fncnv  5158  fun11  5159  dff13  5471  frds  5935  ncssfin  6151  sbth  6206  spacind  6287