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  966  nanass  1510  nic-ax  1673  nic-axALT  1674  tbw-bijust  1698  merco1  1713  19.23v  1942  19.24  1985  hbsbwOLD  2172  sb4a  2485  2eu6  2657  axi5r  2700  ralrexbidOLD  3107  r19.36v  3184  ceqsal1t  3514  spcgft  3549  vtoclgft  3552  elabgt  3672  elabgtOLD  3673  mo2icl  3720  euind  3730  reu6  3732  reuind  3759  sbciegftOLD  3826  elpwunsn  4684  dfiin2g  5032  invdisj  5129  ssrel  5792  ssrelOLD  5793  dff3  7120  fnoprabg  7556  tfindsg  7882  findsg  7919  zfrep6  7979  tz7.48-1  8483  odi  8617  r1sdom  9814  kmlem6  10196  kmlem12  10202  zorng  10544  squeeze0  12171  xrsupexmnf  13347  xrinfmexpnf  13348  mptnn0fsuppd  14039  rexanre  15385  pmatcollpw2lem  22783  tgcnp  23261  lmcvg  23270  iblcnlem  25824  limcresi  25920  isch3  31260  disjexc  32606  ssdifidlprm  33486  cntmeas  34227  bnj900  34943  bnj1172  35015  bnj1174  35017  bnj1176  35019  gonarlem  35399  goalrlem  35401  axextdfeq  35798  hbimtg  35807  nn0prpw  36324  meran3  36414  waj-ax  36415  lukshef-ax2  36416  imsym1  36419  bj-peircestab  36554  bj-orim2  36557  bj-andnotim  36589  bj-ssbid2ALT  36664  bj-19.21bit  36691  bj-substax12  36722  bj-ceqsalt0  36885  bj-ceqsalt1  36886  wl-embant  37511  contrd  38104  ax12indi  38945  ltrnnid  40138  ismrc  42712  frege55lem1a  43879  frege55lem1b  43908  frege55lem1c  43929  frege92  43968  pm11.71  44416  exbir  44499  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  r19.36vf  45141  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  setrec2mpt  49216