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  2511  2eu6  2683  axi5r  2726  r19.36v  3192  ceqsal1t  3485  spcgft  3515  vtoclgft  3518  elabgtOLD  3630  mo2icl  3675  euind  3685  reu6  3687  reuind  3714  elpwunsn  4648  dfiin2g  4993  invdisj  5093  zfrep6  5248  ssrel  5767  dff3  7097  fnoprabg  7540  tfindsg  7861  findsg  7898  zfrep6OLD  7956  tz7.48-1  8436  odi  8570  r1sdom  9760  kmlem6  10162  kmlem12  10168  zorng  10510  squeeze0  12146  xrsupexmnf  13361  xrinfmexpnf  13362  mptnn0fsuppd  14066  rexanre  15438  ssdifidlprm  21555  pmatcollpw2lem  23008  tgcnp  23484  lmcvg  23493  iblcnlem  26023  limcresi  26119  isch3  31730  disjexc  33074  cntmeas  34745  bnj900  35446  bnj1172  35518  bnj1174  35520  bnj1176  35522  r1omhfb  35630  r1omhfbregs  35671  gonarlem  35981  goalrlem  35983  axextdfeq  36382  hbimtg  36391  nn0prpw  36950  meran3  37040  waj-ax  37041  lukshef-ax2  37042  imsym1  37045  axnulregtco  37107  mh-setindnd  37164  bj-peircestab  37259  bj-orim2  37264  bj-andnotim  37297  bj-alextruim  37375  bj-ssbid2ALT  37401  bj-19.21bit  37431  bj-substax12  37465  bj-ceqsalt0  37635  bj-ceqsalt1  37636  bj-rep  37826  bj-axreprepsep  37828  wl-embant  38281  contrd  38853  ax12indi  39825  ltrnnid  41017  ismrc  43554  frege55lem1a  44714  frege55lem1b  44743  frege55lem1c  44764  frege92  44803  pm11.71  45229  exbir  45310  ax6e2ndeqVD  45739  ax6e2ndeqALT  45761  r19.36vf  45976  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  setrec2mpt  50631