Theorem mpan2 422

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	|- ps
mpan2.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpan2	|- ( ph -> ch )

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		mpan2.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpdan 418	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mpanr12  436  mp3an23  1308  equs4  1704  sb4bor  1808  elvd  2694  eueq2dc  2861  sbcgf  2980  csbconstgf  3020  sbcnestg  3058  csbnestg  3059  csbnest1g  3060  ssindif0im  3427  mpteq1  4020  iinexgm  4087  mss  4156  eusv2nf  4385  eldifpw  4406  ordtriexmid  4445  onsucsssucexmid  4450  ordsucunielexmid  4454  nn0suc  4526  xpss1  4657  xpiindim  4684  reldm0  4765  elrnmpt1s  4797  resdm  4866  resid  4883  eliniseg  4917  trinxp  4940  inimasn  4964  ssrnres  4989  cnveq0  5003  coi2  5063  relrelss  5073  funcnvres  5204  funimaex  5216  fnresin1  5245  fnresin2  5246  fresin  5309  dffv3g  5425  ssimaex  5490  dmfco  5497  fvmpt  5506  fsn  5600  fsn2  5602  elabrex  5667  f1elima  5682  2ndconst  6127  tposfun  6165  tpostpos2  6170  tfrexlem  6239  tfri3  6272  rdgruledefgg  6280  rdgss  6288  frecsuclem  6311  frecrdg  6313  oa0  6361  om0  6362  oei0  6363  oav2  6367  oa1suc  6371  nnmsucr  6392  nnm1  6428  nnm2  6429  ecelqsg  6490  ecidg  6501  xpider  6508  qsel  6514  mapdm0  6565  map0e  6588  mapsnconst  6596  ixpsnf1o  6638  map1  6714  xp1en  6725  xpcomco  6728  xpmapenlem  6751  findcard2s  6792  findcard2d  6793  findcard2sd  6794  exmidpw  6810  fidcenumlemr  6851  sbthlem7  6859  eqinfti  6915  djueq1  6933  omp1eomlem  6987  endjusym  6989  eninl  6990  eninr  6991  difinfsn  6993  finomni  7020  pm54.43  7063  exmidonfinlem  7066  mulidpi  7150  nlt1pig  7173  indpi  7174  halfnqq  7242  archnqq  7249  prarloclemarch  7250  prarloclemarch2  7251  nnnq  7254  nq0a0  7289  addpinq1  7296  prarloclemlt  7325  prarloclemlo  7326  prarloclem3  7329  prarloclemcalc  7334  nqprm  7374  addnqpr1  7394  1idprl  7422  1idpru  7423  1idpr  7424  recexprlem1ssl  7465  recexprlem1ssu  7466  ltmprr  7474  0idsr  7599  1idsr  7600  00sr  7601  pn0sr  7603  negexsr  7604  recexgt0sr  7605  ltm1sr  7609  archsr  7614  prsrcl  7616  prsradd  7618  mappsrprg  7636  map2psrprg  7637  elrealeu  7661  pitonnlem1p1  7678  peano2nnnn  7685  ax1rid  7709  axcnre  7713  peano5nnnn  7724  peano2cn  7921  peano2re  7922  addid2  7925  subid  8005  subid1  8006  negid  8033  negeq0  8040  peano2cnm  8052  peano2rem  8053  mul01  8175  lt0neg1  8254  le0neg1  8256  recexre  8364  inelr  8370  rimul  8371  reapmul1  8381  apsqgt0  8387  mulge0  8405  negap0  8416  divvalap  8458  rerecclap  8514  div2negap  8519  divgt0i2i  8699  peano5nni  8747  nnge1  8767  times2  8873  addltmul  8980  nn0p1nn  9040  peano2nn0  9041  nn0lele2xi  9052  znnnlt1  9126  nn0lt10b  9155  prime  9174  msqznn  9175  zeo  9180  elnn1uz2  9428  qreccl  9461  qdivcl  9462  irrmul  9466  rphalfcl  9498  rpnegap  9503  zgt1rpn0n1  9512  ltpnf  9597  nltmnf  9604  pnfge  9605  xlt0neg1  9651  xle0neg1  9653  xaddpnf1  9659  xaddmnf1  9661  xaddid1  9675  xsubge0  9694  xleaddadd  9700  elioopnf  9780  elicopnf  9782  iccshftri  9808  iccshftli  9810  iccdili  9812  icccntri  9814  fzprval  9893  fzofzp1  10035  fzostep1  10045  flqge0nn0  10097  flqge1nn  10098  fldiv4p1lem1div2  10109  exp1  10330  qexpclz  10345  nn0sqcl  10351  expeq0  10355  expubnd  10381  sqval  10382  sqeq0  10387  resqcl  10391  zsqcl  10394  iexpcyc  10428  binom21  10435  bcnn  10535  bcn2  10542  bcn2p1  10548  bcnm1  10550  fihasheq0  10572  hashsng  10576  fihashen1  10577  fimaxq  10605  shftfibg  10624  shftfib  10627  reim0  10665  imval2  10698  cjap0  10711  cjne0  10712  rexuz3  10794  resqrexlemover  10814  abssq  10885  nn0abscl  10889  nnabscl  10904  abs2dif  10910  max0addsup  11023  climshft  11105  bcxmas  11290  efgt1p2  11438  efgt1p  11439  efi4p  11460  resin4p  11461  recos4p  11462  sinbnd  11495  cosbnd  11496  dvdsval2  11532  zdvdsdc  11550  dvdsmul2  11552  dvdsmulcr  11559  dvdsabseq  11581  divconjdvds  11583  alzdvds  11588  fzo0dvdseq  11591  odd2np1lem  11605  mod2eq1n2dvds  11612  flodddiv4  11667  flodddiv4t2lthalf  11670  gcdmndc  11673  gcd0id  11703  gcd1  11711  dfgcd2  11738  gcdmultiple  11744  gcdmultiplez  11745  dvdssq  11755  lcmmndc  11779  lcm0val  11782  dvdslcm  11786  lcmeq0  11788  lcmgcd  11795  lcmdvds  11796  lcmid  11797  lcm1  11798  cncongr2  11821  isprm3  11835  prm2orodd  11843  sqrt2irrap  11894  phiprm  11935  unennn  11946  ennnfonelemim  11973  ctinfom  11977  ctinf  11979  enctlem  11981  ressid  12059  elrestr  12167  0opn  12212  topopn  12214  tgval  12257  tgvalex  12258  0cld  12320  ntropn  12325  ntrtop  12336  ntr0  12342  neipsm  12362  rest0  12387  xmetres  12590  metres  12591  mopnex  12713  tgioo  12754  cnlimcim  12848  cnlimc  12849  dvfre  12882  dveflem  12895  dvef  12896  efcn  12897  sin2pim  12942  cos2pim  12943  sinmpi  12944  cosmpi  12945  sinppi  12946  cosppi  12947  efimpi  12948  sincosq1lem  12954  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  sinq34lt0t  12960  sincosq1eq  12968  abssinper  12975  logrpap0b  13005  loglt1b  13022  rpcxp0  13027  rpcxp1  13028  rpcxpsqrt  13050  logsqrt  13051  rprelogbdiv  13082  bj-inf2vnlem1  13339  pwle2  13366  pwf1oexmid  13367  exmid1stab  13368  nninfsellemeqinf  13387  sbthom  13396  iswomninnlem  13417