Theorem imim2i 16

Description: Inference adding common antecedents in an implication. Inference associated with imim2 58. Its associated inference is syl 17. (Contributed by NM, 28-Dec-1992.)

Hypothesis

Ref	Expression
imim2i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
imim2i	⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

Proof of Theorem imim2i

Step	Hyp	Ref	Expression
1		imim2i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	a2i 14	1 ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim12i  62  imim3i  64  ja  186  imim21b  395  jcab  518  pm3.48  961  nanass  1505  nic-ax  1676  nic-axALT  1677  tbw-bijust  1701  merco1  1716  19.23v  1946  19.24  1990  hbsbw  2170  sb4a  2485  2eu6  2659  axi5r  2702  ralrexbidOLD  3257  r19.36v  3273  ceqsalt  3463  vtoclgft  3493  spcgft  3528  elabgt  3604  mo2icl  3650  euind  3660  reu6  3662  reuind  3689  sbciegft  3755  elpwunsn  4620  dfiin2g  4963  invdisj  5059  ssrel  5694  ssrelOLD  5695  dff3  6985  fnoprabg  7406  tfindsg  7716  findsg  7755  zfrep6  7806  tz7.48-1  8283  odi  8419  r1sdom  9541  kmlem6  9920  kmlem12  9926  zorng  10269  squeeze0  11887  xrsupexmnf  13048  xrinfmexpnf  13049  mptnn0fsuppd  13727  rexanre  15067  pmatcollpw2lem  21935  tgcnp  22413  lmcvg  22422  iblcnlem  24962  limcresi  25058  isch3  29612  disjexc  30941  cntmeas  32203  bnj900  32918  bnj1172  32990  bnj1174  32992  bnj1176  32994  gonarlem  33365  goalrlem  33367  axextdfeq  33782  hbimtg  33791  nn0prpw  34521  meran3  34611  waj-ax  34612  lukshef-ax2  34613  imsym1  34616  bj-peircestab  34742  bj-orim2  34745  bj-andnotim  34779  bj-ssbid2ALT  34853  bj-19.21bit  34881  bj-substax12  34912  bj-ceqsalt0  35078  bj-ceqsalt1  35079  wl-embant  35678  contrd  36264  ax12indi  36965  ltrnnid  38157  ismrc  40530  frege55lem1a  41481  frege55lem1b  41510  frege55lem1c  41531  frege92  41570  pm11.71  42022  exbir  42105  ax6e2ndeqVD  42536  ax6e2ndeqALT  42558  r19.36vf  42692  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977