Theorem imim2i 14

Description: Inference adding common antecedents in an implication. (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 13	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  57  imim3i  59  imim12  97  ja  161  imim21b  367  pm3.48  829  jcab  858  nic-ax  1480  nic-axALT  1481  tbw-bijust  1505  merco1  1520  sbimi  1706  19.24  1715  ax12indi  2245  mopickOLDOLD  2341  2eu6  2371  axi5r  2415  r19.36av  2880  ceqsalt  3007  vtoclgft  3032  spcgft  3061  mo2icl  3150  euind  3158  reu6  3160  reuind  3174  sbciegft  3229  elpwunsn  3929  dfiin2g  4215  invdisj  4293  dff3  5868  fnoprabg  6203  tfindsg  6483  findsg  6515  zfrep6  6557  tz7.48-1  6910  odi  7030  r1sdom  7993  kmlem6  8336  kmlem12  8342  zorng  8685  squeeze0  10247  xrsupexmnf  11279  xrinfmexpnf  11280  rexanre  12846  tgcnp  18869  lmcvg  18878  bwthOLD  19026  iblcnlem  21278  limcresi  21372  isch3  24656  disjexc  25947  cntmeas  26652  axextdfeq  27623  hbimtg  27632  meran3  28271  waj-ax  28272  lukshef-ax2  28273  imsym1  28276  wl-impchain-1-syl  28350  wl-impchain-2-syl  28351  wl-embantALT  28364  nn0prpw  28530  orcomdd  28904  cnf1dd  28905  notornotel1  28910  contrd  28912  ismrc  29049  pm11.71  29662  pmatcollpw2lem  30917  exbir  31166  ax6e2ndeqVD  31657  ax6e2ndeqALT  31679  bnj900  31934  bnj1172  32004  bnj1174  32006  bnj1176  32008  bj-andnotim  32126  bj-19.21bit  32191  bj-ceqsalt0  32396  bj-ceqsalt1  32397  ltrnnid  33792