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  187  imim21b  398  jcab  525  pm3.48  976  nanass  1529  nic-ax  1692  nic-axALT  1693  tbw-bijust  1717  merco1  1732  19.23v  1961  19.24  2010  sb4a  2510  2eu6  2682  axi5r  2725  r19.36v  3189  ceqsal1t  3485  spcgft  3516  vtoclgft  3519  elabgtOLD  3632  mo2icl  3676  euind  3686  reu6  3688  reuind  3715  elpwunsn  4642  dfiin2g  4987  invdisj  5085  zfrep6  5238  ssrel  5753  dff3  7077  fnoprabg  7515  tfindsg  7837  findsg  7874  zfrep6OLD  7932  tz7.48-1  8409  odi  8543  r1sdom  9729  kmlem6  10109  kmlem12  10115  zorng  10458  squeeze0  12092  xrsupexmnf  13305  xrinfmexpnf  13306  mptnn0fsuppd  14008  rexanre  15357  pmatcollpw2lem  22817  tgcnp  23293  lmcvg  23302  iblcnlem  25831  limcresi  25927  isch3  31390  disjexc  32742  ssdifidlprm  33606  cntmeas  34484  bnj900  35188  bnj1172  35260  bnj1174  35262  bnj1176  35264  r1omhfb  35372  r1omhfbregs  35397  gonarlem  35708  goalrlem  35710  axextdfeq  36109  hbimtg  36118  nn0prpw  36647  meran3  36737  waj-ax  36738  lukshef-ax2  36739  imsym1  36742  axnulregtco  36804  mh-setindnd  36861  bj-peircestab  36957  bj-orim2  36962  bj-andnotim  36995  bj-alextruim  37073  bj-ssbid2ALT  37099  bj-19.21bit  37129  bj-substax12  37163  bj-ceqsalt0  37333  bj-ceqsalt1  37334  bj-rep  37522  bj-axreprepsep  37524  wl-embant  37977  contrd  38560  ax12indi  39532  ltrnnid  40724  ismrc  43246  frege55lem1a  44406  frege55lem1b  44435  frege55lem1c  44456  frege92  44495  pm11.71  44937  exbir  45019  ax6e2ndeqVD  45448  ax6e2ndeqALT  45470  r19.36vf  45678  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206  setrec2mpt  50282