Theorem imbi1i 315

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbi1i.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
imbi1i	⊢ ((φ → χ) ↔ (ψ → χ))

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 ⊢ (φ ↔ ψ)
2		imbi1 313	. 2 ⊢ ((φ ↔ ψ) → ((φ → χ) ↔ (ψ → χ)))
3	1, 2	ax-mp 5	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  imor  401  ancomsimp  1369  19.43  1605  19.37  1873  dfsb3  2056  sbor  2066  sbrim  2067  mo4f  2236  2mos  2283  neor  2600  r3al  2671  r19.23t  2728  r19.43  2766  ceqsralt  2882  ralab  2997  ralrab  2998  euind  3023  reu2  3024  rmo4  3029  reuind  3039  2reu5lem3  3043  rmo3  3133  unss  3437  ralunb  3444  inssdif0  3617  ssundif  3633  dfif2  3664  pwss  3736  ralsns  3763  disjsn  3786  snss  3838  unissb  3921  intun  3958  intpr  3959  dfiin2g  4000  eqpw1  4162  pw111  4170  ssrelk  4211  eqrelk  4212  elp6  4263  sikexlem  4295  insklem  4304  peano5  4409  ltfintrilem1  4465  evenodddisjlem1  4515  nnadjoin  4520  nnpweq  4523  raliunxp  4823  intirr  5029  dffun4  5121  dffun5  5122  dffun7  5133  fun11  5159  fununi  5160  dff13  5471  clos1induct  5880  dfnnc3  5885  enmap2lem4  6066  enmap1lem4  6072  spacind  6287