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  1977  19.24  2026  sb4a  2512  2eu6  2684  axi5r  2727  r19.36v  3194  ceqsal1t  3486  spcgft  3516  vtoclgft  3519  elabgtOLD  3630  mo2icl  3675  euind  3685  reu6  3687  reuind  3714  elpwunsn  4645  dfiin2g  4992  invdisj  5092  zfrep6  5245  ssrel  5764  dff3  7124  fnoprabg  7566  tfindsg  7896  findsg  7933  zfrep6OLD  7991  tz7.48-1  8481  odi  8615  r1sdom  9808  kmlem6  10261  kmlem12  10267  zorng  10609  squeeze0  12247  xrsupexmnf  13462  xrinfmexpnf  13463  mptnn0fsuppd  14168  rexanre  15543  ssdifidlprm  21672  pmatcollpw2lem  23125  tgcnp  23601  lmcvg  23610  iblcnlem  26139  limcresi  26235  isch3  31873  disjexc  33259  cntmeas  34929  bnj900  35629  bnj1172  35701  bnj1174  35703  bnj1176  35705  reu6f  35779  eqhf  35820  eqhfregs  35905  gonarlem  36326  goalrlem  36328  axextdfeq  36737  hbimtg  36746  nn0prpw  37289  meran3  37379  waj-ax  37380  lukshef-ax2  37381  imsym1  37384  axnulregtco  37446  mh-setindnd  37503  bj-peircestab  37598  bj-orim2  37603  bj-andnotim  37636  bj-alextruim  37714  bj-ssbid2ALT  37740  bj-19.21bit  37770  bj-substax12  37804  bj-ceqsalt0  37974  bj-ceqsalt1  37975  bj-rep  38180  bj-axreprepsep  38182  wl-embant  38634  contrd  39221  ax12indi  40193  ltrnnid  41385  ismrc  43905  frege55lem1a  45058  frege55lem1b  45087  frege55lem1c  45108  frege92  45147  pm11.71  45573  exbir  45653  ax6e2ndeqVD  46082  ax6e2ndeqALT  46104  r19.36vf  46356  nn0sumshdiglemA  49936  nn0sumshdiglemB  49937  setrec2mpt  51070