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	|- ( ph -> ps )

Assertion

Ref	Expression
imim2i	|- ( ( ch -> ph ) -> ( ch -> ps ) )

Proof of Theorem imim2i

Step	Hyp	Ref	Expression
1		imim2i.1	. . 3 |- ( ph -> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph -> ps ) )
3	2	a2i 14	1 |- ( ( ch -> ph ) -> ( ch -> ps ) )

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  173  imim21b  382  pm3.48  878  jcab  907  nic-ax  1598  nic-axALT  1599  tbw-bijust  1623  merco1  1638  sbimi  1886  19.24  1900  19.23v  1902  2eu6  2558  axi5r  2594  r19.36v  3085  ceqsalt  3228  vtoclgft  3254  vtoclgftOLD  3255  spcgft  3285  mo2icl  3385  euind  3393  reu6  3395  reuind  3411  sbciegft  3466  elpwunsn  4224  dfiin2g  4553  invdisj  4638  ssrel  5207  dff3  6372  fnoprabg  6761  tfindsg  7060  findsg  7093  zfrep6  7134  tz7.48-1  7538  odi  7659  r1sdom  8637  kmlem6  8977  kmlem12  8983  zorng  9326  squeeze0  10926  xrsupexmnf  12135  xrinfmexpnf  12136  mptnn0fsuppd  12798  reuccats1lem  13479  rexanre  14086  pmatcollpw2lem  20582  tgcnp  21057  lmcvg  21066  iblcnlem  23555  limcresi  23649  isch3  28098  disjexc  29406  cntmeas  30289  bnj900  30999  bnj1172  31069  bnj1174  31071  bnj1176  31073  axextdfeq  31703  hbimtg  31712  nn0prpw  32318  meran3  32412  waj-ax  32413  lukshef-ax2  32414  imsym1  32417  bj-orim2  32541  bj-currypeirce  32544  bj-andnotim  32573  bj-ssbequ2  32643  bj-ssbid2ALT  32646  bj-19.21bit  32680  bj-ceqsalt0  32873  bj-ceqsalt1  32874  wl-embant  33293  contrd  33899  ax12indi  34229  ltrnnid  35422  ismrc  37264  rp-fakenanass  37860  frege55lem1a  38160  frege55lem1b  38189  frege55lem1c  38210  frege92  38249  pm11.71  38597  exbir  38684  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  r19.36vf  39324  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414