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  2484  2eu6  2657  axi5r  2700  r19.36v  3165  ceqsal1t  3462  spcgft  3494  vtoclgft  3497  elabgtOLD  3615  elabgtOLDOLD  3616  mo2icl  3660  euind  3670  reu6  3672  reuind  3699  sbciegftOLD  3766  elpwunsn  4628  dfiin2g  4973  invdisj  5071  zfrep6  5224  ssrel  5739  dff3  7052  fnoprabg  7490  tfindsg  7812  findsg  7848  zfrep6OLD  7908  tz7.48-1  8382  odi  8514  r1sdom  9698  kmlem6  10078  kmlem12  10084  zorng  10426  squeeze0  12059  xrsupexmnf  13257  xrinfmexpnf  13258  mptnn0fsuppd  13960  rexanre  15309  pmatcollpw2lem  22742  tgcnp  23218  lmcvg  23227  iblcnlem  25756  limcresi  25852  isch3  31312  disjexc  32663  ssdifidlprm  33518  cntmeas  34370  bnj900  35071  bnj1172  35143  bnj1174  35145  bnj1176  35147  r1omhfb  35256  r1omhfbregs  35281  gonarlem  35576  goalrlem  35578  axextdfeq  35977  hbimtg  35986  nn0prpw  36505  meran3  36595  waj-ax  36596  lukshef-ax2  36597  imsym1  36600  axnulregtco  36662  mh-setindnd  36719  bj-peircestab  36815  bj-orim2  36820  bj-andnotim  36853  bj-alextruim  36931  bj-ssbid2ALT  36957  bj-19.21bit  36987  bj-substax12  37021  bj-ceqsalt0  37191  bj-ceqsalt1  37192  bj-rep  37380  bj-axreprepsep  37382  wl-embant  37835  contrd  38418  ax12indi  39390  ltrnnid  40582  ismrc  43133  frege55lem1a  44293  frege55lem1b  44322  frege55lem1c  44343  frege92  44382  pm11.71  44824  exbir  44906  ax6e2ndeqVD  45335  ax6e2ndeqALT  45357  r19.36vf  45566  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  setrec2mpt  50172