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  1539  nic-ax  1705  nic-axALT  1706  tbw-bijust  1730  merco1  1745  19.23v  1974  19.24  2023  sb4a  2509  2eu6  2681  axi5r  2724  r19.36v  3190  ceqsal1t  3482  spcgft  3512  vtoclgft  3515  elabgtOLD  3626  mo2icl  3671  euind  3681  reu6  3683  reuind  3710  elpwunsn  4641  dfiin2g  4988  invdisj  5088  zfrep6  5241  ssrel  5758  dff3  7100  fnoprabg  7543  tfindsg  7872  findsg  7909  zfrep6OLD  7967  tz7.48-1  8456  odi  8590  r1sdom  9784  kmlem6  10237  kmlem12  10243  zorng  10585  squeeze0  12223  xrsupexmnf  13438  xrinfmexpnf  13439  mptnn0fsuppd  14144  rexanre  15519  ssdifidlprm  21647  pmatcollpw2lem  23100  tgcnp  23576  lmcvg  23585  iblcnlem  26114  limcresi  26210  isch3  31848  disjexc  33234  cntmeas  34905  bnj900  35605  bnj1172  35677  bnj1174  35679  bnj1176  35681  reu6f  35755  r1omhfb  35790  r1omhfbregs  35861  gonarlem  36245  goalrlem  36247  axextdfeq  36651  hbimtg  36660  nn0prpw  37203  meran3  37293  waj-ax  37294  lukshef-ax2  37295  imsym1  37298  axnulregtco  37360  mh-setindnd  37417  bj-peircestab  37512  bj-orim2  37517  bj-andnotim  37550  bj-alextruim  37628  bj-ssbid2ALT  37654  bj-19.21bit  37684  bj-substax12  37718  bj-ceqsalt0  37888  bj-ceqsalt1  37889  bj-rep  38081  bj-axreprepsep  38083  wl-embant  38535  contrd  39122  ax12indi  40094  ltrnnid  41286  ismrc  43805  frege55lem1a  44959  frege55lem1b  44988  frege55lem1c  45009  frege92  45048  pm11.71  45474  exbir  45555  ax6e2ndeqVD  45984  ax6e2ndeqALT  46006  r19.36vf  46244  nn0sumshdiglemA  49824  nn0sumshdiglemB  49825  setrec2mpt  50958