Theorem imim2i 16

Description: Inference adding common antecedents in an implication. Inference associated with imim2 58. Its associated inference is syl 17. (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 14	1 ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim12i  62  imim3i  64  ja  186  imim21b  394  jcab  517  pm3.48  965  nanass  1511  nic-ax  1674  nic-axALT  1675  tbw-bijust  1699  merco1  1714  19.23v  1943  19.24  1992  hbsbwOLD  2175  sb4a  2480  2eu6  2652  axi5r  2695  r19.36v  3160  ceqsal1t  3469  spcgft  3504  vtoclgft  3507  elabgtOLD  3628  elabgtOLDOLD  3629  mo2icl  3673  euind  3683  reu6  3685  reuind  3712  sbciegftOLD  3779  elpwunsn  4637  dfiin2g  4981  invdisj  5077  ssrel  5723  dff3  7033  fnoprabg  7469  tfindsg  7791  findsg  7827  zfrep6  7887  tz7.48-1  8362  odi  8494  r1sdom  9667  kmlem6  10047  kmlem12  10053  zorng  10395  squeeze0  12025  xrsupexmnf  13204  xrinfmexpnf  13205  mptnn0fsuppd  13905  rexanre  15254  pmatcollpw2lem  22693  tgcnp  23169  lmcvg  23178  iblcnlem  25718  limcresi  25814  isch3  31219  disjexc  32571  ssdifidlprm  33421  cntmeas  34237  bnj900  34939  bnj1172  35011  bnj1174  35013  bnj1176  35015  r1omhfb  35121  r1omhfbregs  35131  gonarlem  35436  goalrlem  35438  axextdfeq  35837  hbimtg  35846  nn0prpw  36363  meran3  36453  waj-ax  36454  lukshef-ax2  36455  imsym1  36458  bj-peircestab  36593  bj-orim2  36596  bj-andnotim  36628  bj-ssbid2ALT  36703  bj-19.21bit  36730  bj-substax12  36761  bj-ceqsalt0  36924  bj-ceqsalt1  36925  wl-embant  37550  contrd  38143  ax12indi  38989  ltrnnid  40181  ismrc  42740  frege55lem1a  43905  frege55lem1b  43934  frege55lem1c  43955  frege92  43994  pm11.71  44436  exbir  44518  ax6e2ndeqVD  44947  ax6e2ndeqALT  44969  r19.36vf  45179  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658  setrec2mpt  49735