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 ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim12i  63  imim3i  65  ja  188  imim21b  400  jcab  527  pm3.48  978  nanass  1540  nic-ax  1706  nic-axALT  1707  tbw-bijust  1731  merco1  1746  19.23v  1975  19.24  2024  sb4a  2510  2eu6  2682  axi5r  2725  r19.36v  3191  ceqsal1t  3483  spcgft  3513  vtoclgft  3516  elabgtOLD  3627  mo2icl  3672  euind  3682  reu6  3684  reuind  3711  elpwunsn  4645  dfiin2g  4989  invdisj  5089  zfrep6  5242  ssrel  5759  dff3  7092  fnoprabg  7535  tfindsg  7861  findsg  7898  zfrep6OLD  7956  tz7.48-1  8437  odi  8571  r1sdom  9764  kmlem6  10215  kmlem12  10221  zorng  10563  squeeze0  12201  xrsupexmnf  13416  xrinfmexpnf  13417  mptnn0fsuppd  14121  rexanre  15494  ssdifidlprm  21622  pmatcollpw2lem  23075  tgcnp  23551  lmcvg  23560  iblcnlem  26089  limcresi  26185  isch3  31825  disjexc  33169  cntmeas  34841  bnj900  35542  bnj1172  35614  bnj1174  35616  bnj1176  35618  r1omhfb  35717  r1omhfbregs  35778  gonarlem  36128  goalrlem  36130  axextdfeq  36529  hbimtg  36538  nn0prpw  37081  meran3  37171  waj-ax  37172  lukshef-ax2  37173  imsym1  37176  axnulregtco  37238  mh-setindnd  37295  bj-peircestab  37390  bj-orim2  37395  bj-andnotim  37428  bj-alextruim  37506  bj-ssbid2ALT  37532  bj-19.21bit  37562  bj-substax12  37596  bj-ceqsalt0  37766  bj-ceqsalt1  37767  bj-rep  37957  bj-axreprepsep  37959  wl-embant  38410  contrd  38997  ax12indi  39969  ltrnnid  41161  ismrc  43665  frege55lem1a  44825  frege55lem1b  44854  frege55lem1c  44875  frege92  44914  pm11.71  45340  exbir  45421  ax6e2ndeqVD  45850  ax6e2ndeqALT  45872  r19.36vf  46094  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676  setrec2mpt  50734