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  964  nanass  1507  nic-ax  1671  nic-axALT  1672  tbw-bijust  1696  merco1  1711  19.23v  1941  19.24  1985  hbsbwOLD  2173  sb4a  2488  2eu6  2660  axi5r  2703  ralrexbidOLD  3113  r19.36v  3190  ceqsal1t  3522  spcgft  3561  vtoclgft  3564  elabgt  3685  elabgtOLD  3686  mo2icl  3736  euind  3746  reu6  3748  reuind  3775  sbciegftOLD  3843  elpwunsn  4707  dfiin2g  5055  invdisj  5152  ssrel  5806  ssrelOLD  5807  dff3  7134  fnoprabg  7573  tfindsg  7898  findsg  7937  zfrep6  7995  tz7.48-1  8499  odi  8635  r1sdom  9843  kmlem6  10225  kmlem12  10231  zorng  10573  squeeze0  12198  xrsupexmnf  13367  xrinfmexpnf  13368  mptnn0fsuppd  14049  rexanre  15395  pmatcollpw2lem  22804  tgcnp  23282  lmcvg  23291  iblcnlem  25844  limcresi  25940  isch3  31273  disjexc  32615  ssdifidlprm  33451  cntmeas  34190  bnj900  34905  bnj1172  34977  bnj1174  34979  bnj1176  34981  gonarlem  35362  goalrlem  35364  axextdfeq  35761  hbimtg  35770  nn0prpw  36289  meran3  36379  waj-ax  36380  lukshef-ax2  36381  imsym1  36384  bj-peircestab  36519  bj-orim2  36522  bj-andnotim  36554  bj-ssbid2ALT  36629  bj-19.21bit  36656  bj-substax12  36687  bj-ceqsalt0  36850  bj-ceqsalt1  36851  wl-embant  37464  contrd  38057  ax12indi  38900  ltrnnid  40093  ismrc  42657  frege55lem1a  43828  frege55lem1b  43857  frege55lem1c  43878  frege92  43917  pm11.71  44366  exbir  44449  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  r19.36vf  45038  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  setrec2mpt  48789