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  393  jcab  516  pm3.48  961  nanass  1503  nic-ax  1667  nic-axALT  1668  tbw-bijust  1692  merco1  1707  19.23v  1937  19.24  1981  hbsbwOLD  2161  sb4a  2473  2eu6  2645  axi5r  2688  ralrexbidOLD  3096  r19.36v  3173  ceqsal1t  3493  vtoclgft  3530  spcgft  3572  elabgt  3657  elabgtOLD  3658  mo2icl  3706  euind  3716  reu6  3718  reuind  3745  sbciegftOLD  3812  elpwunsn  4689  dfiin2g  5036  invdisj  5133  ssrel  5784  ssrelOLD  5785  dff3  7109  fnoprabg  7543  tfindsg  7866  findsg  7905  zfrep6  7959  tz7.48-1  8464  odi  8600  r1sdom  9799  kmlem6  10180  kmlem12  10186  zorng  10529  squeeze0  12150  xrsupexmnf  13319  xrinfmexpnf  13320  mptnn0fsuppd  13999  rexanre  15329  pmatcollpw2lem  22723  tgcnp  23201  lmcvg  23210  iblcnlem  25762  limcresi  25858  isch3  31123  disjexc  32462  ssdifidlprm  33270  cntmeas  33976  bnj900  34691  bnj1172  34763  bnj1174  34765  bnj1176  34767  gonarlem  35135  goalrlem  35137  axextdfeq  35524  hbimtg  35533  nn0prpw  35938  meran3  36028  waj-ax  36029  lukshef-ax2  36030  imsym1  36033  bj-peircestab  36159  bj-orim2  36162  bj-andnotim  36196  bj-ssbid2ALT  36270  bj-19.21bit  36298  bj-substax12  36329  bj-ceqsalt0  36493  bj-ceqsalt1  36494  wl-embant  37108  contrd  37701  ax12indi  38546  ltrnnid  39739  ismrc  42263  frege55lem1a  43438  frege55lem1b  43467  frege55lem1c  43488  frege92  43527  pm11.71  43976  exbir  44059  ax6e2ndeqVD  44490  ax6e2ndeqALT  44512  r19.36vf  44642  nn0sumshdiglemA  47878  nn0sumshdiglemB  47879  setrec2mpt  48314