Theorem imim2i 16

Description: Inference adding common antecedents in an implication. Inference associated with imim2 55. 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  59  imim3i  61  imim12  100  ja  165  imim21b  369  pm3.48  844  jcab  874  nic-ax  1556  nic-axALT  1557  tbw-bijust  1581  merco1  1596  sbimi  1803  19.24  1816  19.23v  1818  2eu6  2387  axi5r  2423  r19.36v  2938  ceqsalt  3070  vtoclgft  3096  spcgft  3126  mo2icl  3217  euind  3225  reu6  3227  reuind  3243  sbciegft  3298  elpwunsn  4012  dfiin2g  4311  invdisj  4391  dff3  6035  fnoprabg  6397  tfindsg  6687  findsg  6720  zfrep6  6761  tz7.48-1  7160  odi  7280  r1sdom  8245  kmlem6  8585  kmlem12  8591  zorng  8934  squeeze0  10509  xrsupexmnf  11590  xrinfmexpnf  11591  mptnn0fsuppd  12210  reuccats1lem  12836  rexanre  13409  pmatcollpw2lem  19801  tgcnp  20269  lmcvg  20278  iblcnlem  22746  limcresi  22840  isch3  26894  disjexc  28203  cntmeas  29048  bnj900  29740  bnj1172  29810  bnj1174  29812  bnj1176  29814  axextdfeq  30444  hbimtg  30453  nn0prpw  30979  meran3  31073  waj-ax  31074  lukshef-ax2  31075  imsym1  31078  bj-andnotim  31172  bj-ssbequ2  31256  bj-ssbid2ALT  31259  bj-19.21bit  31283  bj-ceqsalt0  31482  bj-ceqsalt1  31483  wl-embantALT  31847  contrd  32333  ax12indi  32515  ltrnnid  33701  ismrc  35543  rp-fakenanass  36159  frege55lem1a  36462  frege55lem1b  36491  frege55lem1c  36512  frege92  36551  pm11.71  36747  exbir  36833  ax6e2ndeqVD  37306  ax6e2ndeqALT  37328  nn0sumshdiglemA  40483  nn0sumshdiglemB  40484