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  966  nanass  1512  nic-ax  1675  nic-axALT  1676  tbw-bijust  1700  merco1  1715  19.23v  1944  19.24  1993  hbsbwOLD  2178  sb4a  2485  2eu6  2658  axi5r  2701  r19.36v  3166  ceqsal1t  3475  spcgft  3508  vtoclgft  3511  elabgtOLD  3629  elabgtOLDOLD  3630  mo2icl  3674  euind  3684  reu6  3686  reuind  3713  sbciegftOLD  3780  elpwunsn  4643  dfiin2g  4988  invdisj  5086  ssrel  5740  dff3  7054  fnoprabg  7491  tfindsg  7813  findsg  7849  zfrep6  7909  tz7.48-1  8384  odi  8516  r1sdom  9698  kmlem6  10078  kmlem12  10084  zorng  10426  squeeze0  12057  xrsupexmnf  13232  xrinfmexpnf  13233  mptnn0fsuppd  13933  rexanre  15282  pmatcollpw2lem  22733  tgcnp  23209  lmcvg  23218  iblcnlem  25758  limcresi  25854  isch3  31328  disjexc  32679  ssdifidlprm  33550  cntmeas  34403  bnj900  35104  bnj1172  35176  bnj1174  35178  bnj1176  35180  r1omhfb  35287  r1omhfbregs  35312  gonarlem  35607  goalrlem  35609  axextdfeq  36008  hbimtg  36017  nn0prpw  36536  meran3  36626  waj-ax  36627  lukshef-ax2  36628  imsym1  36631  mh-setindnd  36686  bj-peircestab  36772  bj-orim2  36777  bj-andnotim  36810  bj-alextruim  36877  bj-ssbid2ALT  36905  bj-19.21bit  36932  bj-substax12  36964  bj-ceqsalt0  37129  bj-ceqsalt1  37130  bj-rep  37318  bj-axreprepsep  37320  wl-embant  37762  contrd  38345  ax12indi  39317  ltrnnid  40509  ismrc  43055  frege55lem1a  44219  frege55lem1b  44248  frege55lem1c  44269  frege92  44308  pm11.71  44750  exbir  44832  ax6e2ndeqVD  45261  ax6e2ndeqALT  45283  r19.36vf  45492  nn0sumshdiglemA  48976  nn0sumshdiglemB  48977  setrec2mpt  50053