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  833  jcab  863  nic-ax  1506  nic-axALT  1507  tbw-bijust  1531  merco1  1546  sbimi  1746  19.24  1759  19.23v  1761  ax12indi  2275  2eu6  2383  axi5r  2427  r19.36v  3005  ceqsalt  3132  vtoclgft  3157  spcgft  3186  mo2icl  3278  euind  3286  reu6  3288  reuind  3303  sbciegft  3358  elpwunsn  4073  dfiin2g  4365  invdisj  4445  dff3  6045  fnoprabg  6402  tfindsg  6694  findsg  6726  zfrep6  6767  tz7.48-1  7126  odi  7246  r1sdom  8209  kmlem6  8552  kmlem12  8558  zorng  8901  squeeze0  10468  xrsupexmnf  11521  xrinfmexpnf  11522  mptnn0fsuppd  12107  reuccats1lem  12717  rexanre  13191  pmatcollpw2lem  19405  tgcnp  19881  lmcvg  19890  iblcnlem  22321  limcresi  22415  isch3  26286  disjexc  27592  cntmeas  28370  axextdfeq  29426  hbimtg  29435  meran3  30062  waj-ax  30063  lukshef-ax2  30064  imsym1  30067  wl-embantALT  30159  nn0prpw  30325  contrd  30681  ismrc  30817  pm11.71  31486  exbir  33341  ax6e2ndeqVD  33831  ax6e2ndeqALT  33853  bnj900  34109  bnj1172  34179  bnj1174  34181  bnj1176  34183  bj-andnotim  34299  bj-19.21bit  34365  bj-ceqsalt0  34571  bj-ceqsalt1  34572  ltrnnid  35982  rp-fakenanass  37861  frege55lem1a  38015  frege55lem1b  38044  frege55lem1c  38065