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  960  nanass  1502  nic-ax  1677  nic-axALT  1678  tbw-bijust  1702  merco1  1717  19.23v  1946  19.24  1990  hbsbw  2171  sb4a  2484  2eu6  2658  axi5r  2701  ralrexbidOLD  3251  r19.36v  3269  ceqsalt  3452  vtoclgft  3482  spcgft  3517  elabgt  3596  mo2icl  3644  euind  3654  reu6  3656  reuind  3683  sbciegft  3749  elpwunsn  4616  dfiin2g  4958  invdisj  5054  ssrel  5683  dff3  6958  fnoprabg  7375  tfindsg  7682  findsg  7720  zfrep6  7771  tz7.48-1  8244  odi  8372  r1sdom  9463  kmlem6  9842  kmlem12  9848  zorng  10191  squeeze0  11808  xrsupexmnf  12968  xrinfmexpnf  12969  mptnn0fsuppd  13646  rexanre  14986  pmatcollpw2lem  21834  tgcnp  22312  lmcvg  22321  iblcnlem  24858  limcresi  24954  isch3  29504  disjexc  30833  cntmeas  32094  bnj900  32809  bnj1172  32881  bnj1174  32883  bnj1176  32885  gonarlem  33256  goalrlem  33258  axextdfeq  33679  hbimtg  33688  nn0prpw  34439  meran3  34529  waj-ax  34530  lukshef-ax2  34531  imsym1  34534  bj-peircestab  34660  bj-orim2  34663  bj-andnotim  34697  bj-ssbid2ALT  34771  bj-19.21bit  34799  bj-substax12  34830  bj-ceqsalt0  34996  bj-ceqsalt1  34997  wl-embant  35596  contrd  36182  ax12indi  36885  ltrnnid  38077  ismrc  40439  frege55lem1a  41363  frege55lem1b  41392  frege55lem1c  41413  frege92  41452  pm11.71  41904  exbir  41987  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  r19.36vf  42574  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854