Theorem mpan2 425

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 421	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mpanr12  439  mp3an23  1329  equs4  1725  sb4bor  1835  elvd  2742  eueq2dc  2910  sbcgf  3030  csbconstgf  3070  sbcnestg  3110  csbnestg  3111  csbnest1g  3112  ssindif0im  3482  mpteq1  4087  iinexgm  4154  exmid1stab  4208  mss  4226  eusv2nf  4456  eldifpw  4477  ordtriexmid  4520  onsucsssucexmid  4526  ordsucunielexmid  4530  nn0suc  4603  xpss1  4736  xpiindim  4764  reldm0  4845  elrnmpt1s  4877  resdm  4946  resid  4964  eliniseg  4998  trinxp  5022  inimasn  5046  ssrnres  5071  cnveq0  5085  coi2  5145  relrelss  5155  funcnvres  5289  funimaex  5301  fnresin1  5330  fnresin2  5331  fresin  5394  dffv3g  5511  ssimaex  5577  dmfco  5584  fvmpt  5593  fsn  5688  fsn2  5690  elabrex  5758  f1elima  5773  2ndconst  6222  tposfun  6260  tpostpos2  6265  tfrexlem  6334  tfri3  6367  rdgruledefgg  6375  rdgss  6383  frecsuclem  6406  frecrdg  6408  oa0  6457  om0  6458  oei0  6459  oav2  6463  oa1suc  6467  nnmsucr  6488  nnm1  6525  nnm2  6526  ecelqsg  6587  ecidg  6598  xpider  6605  qsel  6611  mapdm0  6662  map0e  6685  mapsnconst  6693  ixpsnf1o  6735  map1  6811  xp1en  6822  xpcomco  6825  xpmapenlem  6848  findcard2s  6889  findcard2d  6890  findcard2sd  6891  exmidpw  6907  fidcenumlemr  6953  sbthlem7  6961  eqinfti  7018  djueq1  7038  omp1eomlem  7092  endjusym  7094  eninl  7095  eninr  7096  difinfsn  7098  finomni  7137  pm54.43  7188  exmidonfinlem  7191  2onetap  7253  mulidpi  7316  nlt1pig  7339  indpi  7340  halfnqq  7408  archnqq  7415  prarloclemarch  7416  prarloclemarch2  7417  nnnq  7420  nq0a0  7455  addpinq1  7462  prarloclemlt  7491  prarloclemlo  7492  prarloclem3  7495  prarloclemcalc  7500  nqprm  7540  addnqpr1  7560  1idprl  7588  1idpru  7589  1idpr  7590  recexprlem1ssl  7631  recexprlem1ssu  7632  ltmprr  7640  0idsr  7765  1idsr  7766  00sr  7767  pn0sr  7769  negexsr  7770  recexgt0sr  7771  ltm1sr  7775  archsr  7780  prsrcl  7782  prsradd  7784  mappsrprg  7802  map2psrprg  7803  elrealeu  7827  pitonnlem1p1  7844  peano2nnnn  7851  ax1rid  7875  axcnre  7879  peano5nnnn  7890  peano2cn  8090  peano2re  8091  addlid  8094  subid  8174  subid1  8175  negid  8202  negeq0  8209  peano2cnm  8221  peano2rem  8222  mul01  8344  lt0neg1  8423  le0neg1  8425  recexre  8533  inelr  8539  rimul  8540  reapmul1  8550  apsqgt0  8556  mulge0  8574  negap0  8585  divvalap  8629  rerecclap  8685  div2negap  8690  divgt0i2i  8872  peano5nni  8920  nnge1  8940  times2  9046  addltmul  9153  nn0p1nn  9213  peano2nn0  9214  nn0lele2xi  9225  znnnlt1  9299  nn0lt10b  9331  prime  9350  msqznn  9351  zeo  9356  elnn1uz2  9605  qreccl  9640  qdivcl  9641  irrmul  9645  rphalfcl  9679  rpnegap  9684  zgt1rpn0n1  9693  ltpnf  9778  nltmnf  9786  pnfge  9787  xlt0neg1  9836  xle0neg1  9838  xaddpnf1  9844  xaddmnf1  9846  xaddid1  9860  xsubge0  9879  xleaddadd  9885  elioopnf  9965  elicopnf  9967  iccshftri  9993  iccshftli  9995  iccdili  9997  icccntri  9999  fzprval  10079  fzofzp1  10224  fzostep1  10234  flqge0nn0  10290  flqge1nn  10291  fldiv4p1lem1div2  10302  exp1  10523  qexpclz  10538  nn0sqcl  10544  expeq0  10548  expubnd  10574  sqval  10575  sqeq0  10580  resqcl  10584  zsqcl  10587  iexpcyc  10621  binom21  10629  bcnn  10732  bcn2  10739  bcn2p1  10745  bcnm1  10747  fihasheq0  10768  hashsng  10773  fihashen1  10774  fimaxq  10802  shftfibg  10824  shftfib  10827  reim0  10865  imval2  10898  cjap0  10911  cjne0  10912  rexuz3  10994  resqrexlemover  11014  abssq  11085  nn0abscl  11089  nnabscl  11104  abs2dif  11110  max0addsup  11223  climshft  11307  bcxmas  11492  efgt1p2  11698  efgt1p  11699  efi4p  11720  resin4p  11721  recos4p  11722  sinbnd  11755  cosbnd  11756  dvdsval2  11792  zdvdsdc  11814  dvdsmul2  11816  dvdsmulcr  11823  dvdsabseq  11847  divconjdvds  11849  alzdvds  11854  fzo0dvdseq  11857  odd2np1lem  11871  mod2eq1n2dvds  11878  flodddiv4  11933  flodddiv4t2lthalf  11936  gcdmndc  11939  gcd0id  11974  gcd1  11982  dfgcd2  12009  gcdmultiple  12015  gcdmultiplez  12016  dvdssq  12026  lcmmndc  12056  lcm0val  12059  dvdslcm  12063  lcmeq0  12065  lcmgcd  12072  lcmdvds  12073  lcmid  12074  lcm1  12075  cncongr2  12098  isprm3  12112  prm2orodd  12120  sqrt2irrap  12174  phiprm  12217  pc0  12298  pcdvdstr  12320  unennn  12392  ennnfonelemim  12419  ctinfom  12423  ctinf  12425  enctlem  12427  elrestr  12686  mulg1  12944  mulgnegnn  12947  subrgintm  13324  0opn  13397  topopn  13399  tgval  13442  tgvalex  13443  0cld  13505  ntropn  13510  ntrtop  13521  ntr0  13527  neipsm  13547  rest0  13572  xmetres  13775  metres  13776  mopnex  13898  tgioo  13939  cnlimcim  14033  cnlimc  14034  dvfre  14067  dveflem  14080  dvef  14081  efcn  14082  sin2pim  14127  cos2pim  14128  sinmpi  14129  cosmpi  14130  sinppi  14131  cosppi  14132  efimpi  14133  sincosq1lem  14139  sincosq2sgn  14141  sincosq3sgn  14142  sincosq4sgn  14143  sinq12gt0  14144  sinq34lt0t  14145  sincosq1eq  14153  abssinper  14160  logrpap0b  14190  loglt1b  14207  rpcxp0  14212  rpcxp1  14213  rpcxpsqrt  14235  logsqrt  14236  rprelogbdiv  14268  lgs0  14307  lgs2  14311  lgsneg  14318  lgsdilem  14321  lgsdir2lem2  14323  lgsdir2lem4  14325  lgsdir2lem5  14326  lgsne0  14332  bj-inf2vnlem1  14604  pwle2  14630  pwf1oexmid  14631  nninfsellemeqinf  14647  sbthom  14656  iswomninnlem  14679  redc0  14687