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  188  imim21b  397  jcab  520  pm3.48  960  nanass  1499  nic-ax  1670  nic-axALT  1671  tbw-bijust  1695  merco1  1710  19.23v  1939  19.24  1988  sb4a  2505  sbimiOLD  2511  sbimiALT  2573  2eu6  2740  axi5r  2783  ralrexbid  3322  r19.36v  3342  ceqsalt  3527  vtoclgft  3553  vtoclgftOLD  3554  spcgft  3586  mo2icl  3704  euind  3714  reu6  3716  reuind  3743  sbciegft  3807  elpwunsn  4614  dfiin2g  4949  invdisj  5042  ssrel  5651  dff3  6860  fnoprabg  7269  tfindsg  7569  findsg  7603  zfrep6  7650  tz7.48-1  8073  odi  8199  r1sdom  9197  kmlem6  9575  kmlem12  9581  zorng  9920  squeeze0  11537  xrsupexmnf  12692  xrinfmexpnf  12693  mptnn0fsuppd  13360  rexanre  14700  pmatcollpw2lem  21379  tgcnp  21855  lmcvg  21864  iblcnlem  24383  limcresi  24477  isch3  29012  disjexc  30337  cntmeas  31480  bnj900  32196  bnj1172  32268  bnj1174  32270  bnj1176  32272  gonarlem  32636  goalrlem  32638  axextdfeq  33037  hbimtg  33046  nn0prpw  33666  meran3  33756  waj-ax  33757  lukshef-ax2  33758  imsym1  33761  bj-peircestab  33883  bj-orim2  33886  bj-andnotim  33917  bj-ssbid2ALT  33991  bj-19.21bit  34019  bj-ceqsalt0  34195  bj-ceqsalt1  34196  wl-embant  34744  contrd  35369  ax12indi  36074  ltrnnid  37266  ismrc  39291  frege55lem1a  40205  frege55lem1b  40234  frege55lem1c  40255  frege92  40294  pm11.71  40722  exbir  40805  ax6e2ndeqVD  41236  ax6e2ndeqALT  41258  r19.36vf  41397  nn0sumshdiglemA  44673  nn0sumshdiglemB  44674