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  394  jcab  517  pm3.48  965  nanass  1510  nic-ax  1673  nic-axALT  1674  tbw-bijust  1698  merco1  1713  19.23v  1942  19.24  1991  hbsbwOLD  2173  sb4a  2485  2eu6  2657  axi5r  2700  r19.36v  3170  ceqsal1t  3498  spcgft  3533  vtoclgft  3536  elabgt  3656  elabgtOLD  3657  mo2icl  3702  euind  3712  reu6  3714  reuind  3741  sbciegftOLD  3808  elpwunsn  4665  dfiin2g  5013  invdisj  5110  ssrel  5766  ssrelOLD  5767  dff3  7095  fnoprabg  7535  tfindsg  7861  findsg  7898  zfrep6  7958  tz7.48-1  8462  odi  8596  r1sdom  9793  kmlem6  10175  kmlem12  10181  zorng  10523  squeeze0  12150  xrsupexmnf  13326  xrinfmexpnf  13327  mptnn0fsuppd  14021  rexanre  15370  pmatcollpw2lem  22720  tgcnp  23196  lmcvg  23205  iblcnlem  25747  limcresi  25843  isch3  31227  disjexc  32579  ssdifidlprm  33478  cntmeas  34262  bnj900  34965  bnj1172  35037  bnj1174  35039  bnj1176  35041  gonarlem  35421  goalrlem  35423  axextdfeq  35820  hbimtg  35829  nn0prpw  36346  meran3  36436  waj-ax  36437  lukshef-ax2  36438  imsym1  36441  bj-peircestab  36576  bj-orim2  36579  bj-andnotim  36611  bj-ssbid2ALT  36686  bj-19.21bit  36713  bj-substax12  36744  bj-ceqsalt0  36907  bj-ceqsalt1  36908  wl-embant  37533  contrd  38126  ax12indi  38967  ltrnnid  40160  ismrc  42699  frege55lem1a  43865  frege55lem1b  43894  frege55lem1c  43915  frege92  43954  pm11.71  44396  exbir  44479  ax6e2ndeqVD  44908  ax6e2ndeqALT  44930  r19.36vf  45140  nn0sumshdiglemA  48579  nn0sumshdiglemB  48580  setrec2mpt  49541