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  imim12  105  ja  174  imim21b  383  jcab  513  pm3.48  986  nanass  1631  nanassOLD  1632  nic-ax  1768  nic-axALT  1769  tbw-bijust  1793  merco1  1808  19.23v  2037  sbimi  2068  19.24  2082  19.23vOLD  2084  2eu6  2680  axi5r  2735  r19.36v  3232  ceqsalt  3381  vtoclgft  3407  spcgft  3437  mo2icl  3544  euind  3552  reu6  3554  reuind  3572  sbciegft  3627  elpwunsn  4381  dfiin2g  4709  invdisj  4795  ssrel  5377  dff3  6562  fnoprabg  6959  tfindsg  7258  findsg  7291  zfrep6  7332  tz7.48-1  7742  odi  7864  r1sdom  8852  kmlem6  9230  kmlem12  9236  zorng  9579  squeeze0  11180  xrsupexmnf  12337  xrinfmexpnf  12338  mptnn0fsuppd  13005  reuccats1lemOLD  13725  rexanre  14373  pmatcollpw2lem  20861  tgcnp  21337  lmcvg  21346  iblcnlem  23846  limcresi  23940  isch3  28489  disjexc  29789  cntmeas  30671  bnj900  31379  bnj1172  31449  bnj1174  31451  bnj1176  31453  axextdfeq  32078  hbimtg  32087  nn0prpw  32693  meran3  32783  waj-ax  32784  lukshef-ax2  32785  imsym1  32788  bj-orim2  32911  bj-currypeirce  32913  bj-andnotim  32941  bj-ssbequ2  33011  bj-ssbid2ALT  33014  bj-19.21bit  33048  bj-ceqsalt0  33230  bj-ceqsalt1  33231  wl-embant  33658  contrd  34253  ax12indi  34832  ltrnnid  36024  ismrc  37874  frege55lem1a  38766  frege55lem1b  38795  frege55lem1c  38816  frege92  38855  pm11.71  39203  exbir  39288  ax6e2ndeqVD  39729  ax6e2ndeqALT  39751  r19.36vf  39905  nn0sumshdiglemA  43014  nn0sumshdiglemB  43015