Theorem imim2i 17

Description: Inference adding common antecedents in an implication. Inference associated with imim2 59. Its associated inference is syl 18. (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 15	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  63  imim3i  65  ja  188  imim21b  399  jcab  526  pm3.48  978  nanass  1540  nic-ax  1703  nic-axALT  1704  tbw-bijust  1728  merco1  1743  19.23v  1972  19.24  2021  sb4a  2512  2eu6  2684  axi5r  2727  r19.36v  3193  ceqsal1t  3487  spcgft  3518  vtoclgft  3521  elabgtOLD  3633  mo2icl  3678  euind  3688  reu6  3690  reuind  3717  elpwunsn  4651  dfiin2g  4996  invdisj  5096  zfrep6  5251  ssrel  5771  dff3  7097  fnoprabg  7535  tfindsg  7858  findsg  7895  zfrep6OLD  7953  tz7.48-1  8431  odi  8565  r1sdom  9747  kmlem6  10140  kmlem12  10146  zorng  10489  squeeze0  12119  xrsupexmnf  13332  xrinfmexpnf  13333  mptnn0fsuppd  14036  rexanre  15400  ssdifidlprm  21467  pmatcollpw2lem  22915  tgcnp  23391  lmcvg  23400  iblcnlem  25929  limcresi  26025  isch3  31571  disjexc  32916  cntmeas  34594  bnj900  35295  bnj1172  35367  bnj1174  35369  bnj1176  35371  r1omhfb  35486  r1omhfbregs  35528  gonarlem  35864  goalrlem  35866  axextdfeq  36265  hbimtg  36274  nn0prpw  36812  meran3  36902  waj-ax  36903  lukshef-ax2  36904  imsym1  36907  axnulregtco  36969  mh-setindnd  37026  bj-peircestab  37121  bj-orim2  37126  bj-andnotim  37159  bj-alextruim  37237  bj-ssbid2ALT  37263  bj-19.21bit  37293  bj-substax12  37327  bj-ceqsalt0  37497  bj-ceqsalt1  37498  bj-rep  37688  bj-axreprepsep  37690  wl-embant  38143  contrd  38724  ax12indi  39696  ltrnnid  40888  ismrc  43412  frege55lem1a  44572  frege55lem1b  44601  frege55lem1c  44622  frege92  44661  pm11.71  45087  exbir  45168  ax6e2ndeqVD  45597  ax6e2ndeqALT  45619  r19.36vf  45834  nn0sumshdiglemA  49376  nn0sumshdiglemB  49377  setrec2mpt  50452