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  1510  nic-ax  1673  nic-axALT  1674  tbw-bijust  1698  merco1  1713  19.23v  1942  19.24  1991  hbsbwOLD  2173  sb4a  2478  2eu6  2650  axi5r  2693  r19.36v  3162  ceqsal1t  3480  spcgft  3515  vtoclgft  3518  elabgtOLD  3639  elabgtOLDOLD  3640  mo2icl  3685  euind  3695  reu6  3697  reuind  3724  sbciegftOLD  3791  elpwunsn  4648  dfiin2g  4996  invdisj  5093  ssrel  5745  ssrelOLD  5746  dff3  7072  fnoprabg  7512  tfindsg  7837  findsg  7873  zfrep6  7933  tz7.48-1  8411  odi  8543  r1sdom  9727  kmlem6  10109  kmlem12  10115  zorng  10457  squeeze0  12086  xrsupexmnf  13265  xrinfmexpnf  13266  mptnn0fsuppd  13963  rexanre  15313  pmatcollpw2lem  22664  tgcnp  23140  lmcvg  23149  iblcnlem  25690  limcresi  25786  isch3  31170  disjexc  32522  ssdifidlprm  33429  cntmeas  34216  bnj900  34919  bnj1172  34991  bnj1174  34993  bnj1176  34995  gonarlem  35381  goalrlem  35383  axextdfeq  35785  hbimtg  35794  nn0prpw  36311  meran3  36401  waj-ax  36402  lukshef-ax2  36403  imsym1  36406  bj-peircestab  36541  bj-orim2  36544  bj-andnotim  36576  bj-ssbid2ALT  36651  bj-19.21bit  36678  bj-substax12  36709  bj-ceqsalt0  36872  bj-ceqsalt1  36873  wl-embant  37498  contrd  38091  ax12indi  38937  ltrnnid  40130  ismrc  42689  frege55lem1a  43855  frege55lem1b  43884  frege55lem1c  43905  frege92  43944  pm11.71  44386  exbir  44469  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  r19.36vf  45130  nn0sumshdiglemA  48605  nn0sumshdiglemB  48606  setrec2mpt  49683