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  395  jcab  518  pm3.48  961  nanass  1507  nic-ax  1674  nic-axALT  1675  tbw-bijust  1699  merco1  1714  19.23v  1944  19.24  1988  hbsbw  2168  sb4a  2482  2eu6  2656  axi5r  2699  ralrexbidOLD  3106  r19.36v  3176  ceqsalt  3471  vtoclgft  3501  spcgft  3536  elabgt  3613  mo2icl  3660  euind  3670  reu6  3672  reuind  3699  sbciegft  3765  elpwunsn  4632  dfiin2g  4980  invdisj  5077  ssrel  5725  ssrelOLD  5726  dff3  7033  fnoprabg  7460  tfindsg  7776  findsg  7815  zfrep6  7866  tz7.48-1  8345  odi  8482  r1sdom  9632  kmlem6  10013  kmlem12  10019  zorng  10362  squeeze0  11980  xrsupexmnf  13141  xrinfmexpnf  13142  mptnn0fsuppd  13820  rexanre  15158  pmatcollpw2lem  22033  tgcnp  22511  lmcvg  22520  iblcnlem  25060  limcresi  25156  isch3  29892  disjexc  31219  cntmeas  32492  bnj900  33208  bnj1172  33280  bnj1174  33282  bnj1176  33284  gonarlem  33655  goalrlem  33657  axextdfeq  34058  hbimtg  34067  nn0prpw  34651  meran3  34741  waj-ax  34742  lukshef-ax2  34743  imsym1  34746  bj-peircestab  34872  bj-orim2  34875  bj-andnotim  34909  bj-ssbid2ALT  34983  bj-19.21bit  35011  bj-substax12  35042  bj-ceqsalt0  35207  bj-ceqsalt1  35208  wl-embant  35825  contrd  36411  ax12indi  37262  ltrnnid  38455  ismrc  40836  frege55lem1a  41847  frege55lem1b  41876  frege55lem1c  41897  frege92  41936  pm11.71  42388  exbir  42471  ax6e2ndeqVD  42902  ax6e2ndeqALT  42924  r19.36vf  43058  nn0sumshdiglemA  46383  nn0sumshdiglemB  46384