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  2515  2eu6  2687  axi5r  2730  r19.36v  3196  ceqsal1t  3490  spcgft  3520  vtoclgft  3523  elabgtOLD  3635  mo2icl  3680  euind  3690  reu6  3692  reuind  3719  elpwunsn  4655  dfiin2g  5000  invdisj  5100  zfrep6  5255  ssrel  5774  dff3  7102  fnoprabg  7546  tfindsg  7866  findsg  7903  zfrep6OLD  7961  tz7.48-1  8439  odi  8573  r1sdom  9756  kmlem6  10158  kmlem12  10164  zorng  10506  squeeze0  12136  xrsupexmnf  13349  xrinfmexpnf  13350  mptnn0fsuppd  14054  rexanre  15424  ssdifidlprm  21523  pmatcollpw2lem  22971  tgcnp  23447  lmcvg  23456  iblcnlem  25985  limcresi  26081  isch3  31630  disjexc  32975  cntmeas  34648  bnj900  35349  bnj1172  35421  bnj1174  35423  bnj1176  35425  r1omhfb  35533  r1omhfbregs  35574  gonarlem  35907  goalrlem  35909  axextdfeq  36308  hbimtg  36317  nn0prpw  36875  meran3  36965  waj-ax  36966  lukshef-ax2  36967  imsym1  36970  axnulregtco  37032  mh-setindnd  37089  bj-peircestab  37184  bj-orim2  37189  bj-andnotim  37222  bj-alextruim  37300  bj-ssbid2ALT  37326  bj-19.21bit  37356  bj-substax12  37390  bj-ceqsalt0  37560  bj-ceqsalt1  37561  bj-rep  37751  bj-axreprepsep  37753  wl-embant  38206  contrd  38787  ax12indi  39759  ltrnnid  40951  ismrc  43473  frege55lem1a  44633  frege55lem1b  44662  frege55lem1c  44683  frege92  44722  pm11.71  45148  exbir  45229  ax6e2ndeqVD  45658  ax6e2ndeqALT  45680  r19.36vf  45895  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441  setrec2mpt  50516