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  831  jcab  861  nic-ax  1490  nic-axALT  1491  tbw-bijust  1515  merco1  1530  sbimi  1717  19.24  1726  19.23v  1932  ax12indi  2267  mopickOLDOLD  2363  2eu6  2393  axi5r  2437  r19.36av  3014  ceqsalt  3141  vtoclgft  3166  spcgft  3195  mo2icl  3287  euind  3295  reu6  3297  reuind  3312  sbciegft  3367  elpwunsn  4074  dfiin2g  4364  invdisj  4442  dff3  6045  fnoprabg  6398  tfindsg  6690  findsg  6722  zfrep6  6763  tz7.48-1  7120  odi  7240  r1sdom  8204  kmlem6  8547  kmlem12  8553  zorng  8896  squeeze0  10460  xrsupexmnf  11508  xrinfmexpnf  11509  mptnn0fsuppd  12084  reuccats1lem  12684  rexanre  13158  pmatcollpw2lem  19145  tgcnp  19620  lmcvg  19629  bwthOLD  19777  iblcnlem  22061  limcresi  22155  isch3  25990  disjexc  27283  cntmeas  28029  axextdfeq  29164  hbimtg  29173  meran3  29812  waj-ax  29813  lukshef-ax2  29814  imsym1  29817  wl-embantALT  29909  nn0prpw  30075  contrd  30431  ismrc  30567  pm11.71  31211  exbir  32704  ax6e2ndeqVD  33195  ax6e2ndeqALT  33217  bnj900  33472  bnj1172  33542  bnj1174  33544  bnj1176  33546  bj-andnotim  33664  bj-19.21bit  33731  bj-ceqsalt0  33936  bj-ceqsalt1  33937  ltrnnid  35338  bj-frege55lem1a  37284  frege55lem1b  37296  frege55lem1c  37317