Theorem mp2an 430

Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)

Hypotheses

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

Assertion

Ref	Expression
mp2an	|- ch

Proof of Theorem mp2an

Step	Hyp	Ref	Expression
1		mp2an.2	. 2 |- ps
2		mp2an.1	. . 3 |- ph
3		mp2an.3	. . 3 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpan 428	. 2 |- ( ps -> ch )
5	1, 4	ax-mp 5	1 |- ch

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp4an  431  jaoi  728  mp3an  1378  barbara  2185  eqeq12i  2252  el2v  2827  vtocl2  2878  spc2ev  2921  sbc2ie  3123  csbieb  3189  sseq12i  3276  uneq12i  3381  ineq12i  3430  ifssun  3655  nelpri  3733  ralpr  3764  rexpr  3765  preq12i  3793  dfop  3903  opeq12i  3909  breq12i  4140  mpteq2ia  4219  exmidundif  4345  exmidundifim  4346  opex  4371  opi2  4375  opth2  4382  opeqsn  4395  opeqpr  4396  uniop  4398  opelopaba  4410  braba  4411  opelopab  4416  brab  4417  opelopabaf  4418  unex  4589  snnex  4596  op1stb  4626  ifelpwun  4631  ifex  4634  onun2i  4640  onsucssi  4655  ontriexmidim  4671  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  opthreg  4705  tfis  4732  finds  4749  finds2  4750  nnregexmid  4770  xpeq12i  4798  opelvv  4827  eqrelriiv  4871  eqrelrdv  4873  xpss  4885  xpex  4893  relop  4932  brco  4953  opelcnv  4964  brcnv  4965  asymref  5176  codir  5179  ssrnres  5233  dmprop  5265  dfco2  5290  cossxp  5313  cocnvss  5316  coex  5336  funsn  5432  fnsn  5438  feq23i  5531  resasplitss  5572  fabex  5583  fvex  5718  xpsn  5888  fmptap  5908  opabex  5944  rinvf1o  6038  acexmidlemv  6086  oveq12i  6100  oprabid  6120  oprabss  6177  caovcom  6250  opabex3  6355  iunex  6356  oprabex  6365  ofmres  6373  op1st  6384  op2nd  6385  fo1st  6395  fo2nd  6396  mpoex  6454  1stconst  6461  2ndconst  6462  algrflem  6469  dftpos4  6539  tpostpos  6540  tpossym  6552  frecex  6670  frecfnom  6677  2oex  6709  sucinc  6723  fnoei  6730  oeiexg  6731  nnacli  6760  nnmcli  6761  elec  6853  ecovcom  6921  ecovass  6923  ecovdi  6925  fnmap  6934  mapval  6939  elmap  6963  elpm  6965  elpm2  6966  map0  6977  ixpconst  6996  entri  7079  endisj  7128  xpcomco  7130  phplem2  7160  1ndom2  7172  ssfiexmid  7184  domfiexmid  7188  exmidpw2en  7225  unfiexmid  7231  unfiin  7239  inresflem  7406  casefun  7431  caserel  7433  caseinj  7435  omp1eomlem  7440  omp1eom  7441  endjusym  7442  djufun  7450  djuinj  7452  ctssdccl  7457  ctssdclemr  7458  nninfex  7467  infnninf  7470  fodjuomnilemdc  7490  ctssexmid  7496  exmidonfinlem  7551  dju1p1e2  7555  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  pw1dom2  7592  onntri35  7602  onntri45  7606  2oneel  7628  2omotaplemst  7630  acnccim  7644  1lt2pi  7713  indpi  7715  1nq  7739  rec1nq  7768  1lt2nq  7779  ltaddnq  7780  halfnqq  7783  prarloclemarch2  7792  prarloclemlt  7866  prarloclemcalc  7875  genpelxp  7884  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  cauappcvgprlemladd  8031  caucvgprlemcl  8049  caucvgprprlemcl  8077  suplocexprlemell  8086  suplocexprlemdisj  8093  suplocexprlemub  8096  0r  8123  1sr  8124  m1r  8125  m1p1sr  8133  m1m1sr  8134  0lt1sr  8138  1ne0sr  8139  1idsr  8141  recexgt0sr  8146  prsradd  8159  caucvgsrlemoffres  8173  caucvgsr  8175  mappsrprg  8177  map2psrprg  8178  pitonnlem1p1  8219  pitonnlem2  8220  pitoregt0  8222  peano2nnnn  8226  axi2m1  8248  axprecex  8253  axcnre  8254  nnindnn  8266  nntopi  8267  0cn  8324  addcli  8336  mulcli  8337  mulcomi  8338  readdcli  8345  remulcli  8346  rexpssxrxp  8376  ltrelxr  8392  gtneii  8428  lttri3i  8430  letri3i  8431  ltnsymi  8432  lenlti  8433  ltlei  8434  mulgt0i  8442  mulgt0ii  8443  0lt1  8460  addcomi  8477  pncan3oi  8549  resubcli  8596  subcli  8609  pncan3i  8610  negsubi  8611  subnegi  8612  subeq0i  8613  neg11i  8614  negcon1i  8615  negcon2i  8616  mulneg1i  8738  mulneg2i  8739  mul2negi  8740  addgt0ii  8826  ltnegi  8828  lenegi  8829  ltnegcon2i  8830  lesub0i  8831  ltaddposi  8832  posdifi  8833  ltnegcon1i  8834  lenegcon1i  8835  subge0i  8836  1ap0  8926  ltapii  8971  recrecapi  9082  dividapi  9083  div0api  9084  rec11apii  9099  divdiv32api  9105  recgt0ii  9245  ltrecii  9256  ltdiv23ii  9265  sup3exmid  9295  nnssre  9317  nnind  9329  nnmulcli  9335  nnsubi  9353  0le2  9403  1lt3  9487  2lt4  9489  1lt4  9490  3lt5  9492  2lt5  9493  1lt5  9494  4lt6  9496  3lt6  9497  2lt6  9498  1lt6  9499  5lt7  9501  4lt7  9502  3lt7  9503  2lt7  9504  1lt7  9505  6lt8  9507  5lt8  9508  4lt8  9509  3lt8  9510  2lt8  9511  1lt8  9512  7lt9  9514  6lt9  9515  5lt9  9516  4lt9  9517  3lt9  9518  2lt9  9519  1lt9  9520  2muline0  9541  nn0addcli  9611  nn0mulcli  9612  nn0addge1i  9622  nn0addge2i  9623  dfz2  9726  halfnz  9752  9p1e10  9789  numnncl  9796  numltc  9817  le9lt10  9818  nummac  9836  8lt10  9923  7lt10  9924  6lt10  9925  5lt10  9926  4lt10  9927  3lt10  9928  2lt10  9929  1lt10  9930  eluzaddi  9964  eluzsubi  9965  uzuzle23  9977  uzuzle24  9978  uzuzle34  9979  eluz2nn  9981  eluz4eluz2  9983  eluzge3nn  9987  divfnzn  10036  elq  10037  qreccl  10057  xrltnr  10197  mnfltpnf  10203  xaddmnf1  10266  pnfaddmnf  10268  mnfaddpnf  10269  xrex  10274  xaddid1  10280  xsubge0  10299  xposdif  10300  xleaddadd  10305  elicc2i  10357  ioomax  10366  iccmax  10367  ioopos  10368  elxrge0  10396  iccshftri  10413  iccshftli  10415  iccdili  10417  icccntri  10419  unitssre  10424  fz10  10466  fz00m1  10467  fzpreddisj  10494  fz0to4untppr  10547  dfrp2  10714  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  frecfzennn  10883  xnn0nnen  10894  fnn0nninf  10895  fxnn0nninf  10896  0tonninf  10897  1tonninf  10898  m1expcl2  11018  m1expcl  11019  nn0expcli  11022  sqmuli  11079  cu2  11095  i3  11098  subsqi  11106  binom2subi  11112  bcpasc  11225  4bc2eq6  11234  hashinfom  11238  prhash2ex  11271  hashp1i  11272  lsw0g  11374  swrdccat3blem  11532  rei  11686  imi  11687  readdi  11715  imaddi  11716  remuli  11717  immuli  11718  cjaddi  11719  cjmuli  11720  ipcni  11721  crrei  11723  crimi  11724  rexfiuz  11776  sqrt1  11833  sqrt4  11834  sqrt9  11835  abs1  11859  sqrtmulii  11922  abslti  11926  abslei  11927  abssubi  11938  absmuli  11939  sqabsaddi  11940  sqabssubi  11941  abstrii  11943  fimaxre2  12015  fiidxsupcl  12017  climz  12082  abscn2  12105  recn2  12107  imcn2  12108  climabs  12110  climre  12112  climim  12113  fsumcnv  12228  fsumrelem  12262  fsumre  12263  fsumim  12264  arisum2  12290  expcnv  12295  geo2sum2  12306  geo2lim  12307  0.999...  12312  geoihalfsum  12313  fprodcnv  12416  fprodge0  12428  fprodge1  12430  ege2le3  12462  ef0  12463  reeff1  12491  tan0  12522  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  cos1bnd  12550  cos2bnd  12551  sinltxirr  12552  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  sincos1sgn  12556  sincos2sgn  12557  cos12dec  12559  egt2lt3  12571  epos  12572  ene1  12576  eap1  12577  3dvds  12655  3dvdsdec  12656  3dvds2dec  12657  odd2np1lem  12663  n2dvds1  12703  z4even  12707  ndvdsi  12724  flodddiv4  12727  bitsp1o  12744  0bits  12750  gcd0val  12761  6gcd4e2  12796  3lcm2e6woprm  12888  6lcm4e12  12889  3lcm2e6  12963  sqrt2irrlem  12964  phimullem  13031  pockthi  13165  4sqlem19  13216  dec2dvds  13218  dec5dvds2  13220  dec2nprm  13222  modxai  13223  mod2xnegi  13226  gcdi  13228  gcdmodi  13229  numexpp1  13232  karatsuba  13238  2exp7  13242  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilemofi  13276  ballotfilem1  13277  ballotfilem2  13285  ballotfilemfmpn  13291  ballotfilemefi  13294  ballotfilemodife  13297  ballotfilem4  13298  ballotfilemiex  13301  ballotfilemimin  13306  ballotfilemic  13307  ballotfilemsval  13309  ballotfilemsdom  13312  ballotfilemsel1i  13313  ballotfilemsima  13316  ballotfilemrval  13318  ballotfilemfrceq  13329  ballotfilemfrcn0  13330  ballotfilem1ri  13335  ballotfilem7  13336  ballotfilem8  13337  ballotfilemth  13338  xpnnen  13342  xpomen  13343  ennnfonelemj0  13349  ennnfonelem0  13353  ennnfonelemhf1o  13361  exmidunben  13374  qnnen  13379  unct  13390  setscom  13449  strleun  13516  prdsvallem  13679  imasival  13685  ismgm  13735  fn0g  13753  fngzsum  13766  issgrp  13776  ismnddef  13789  isghm  14104  prdsex  14278  isrng  14339  rngmgpf  14342  isring  14410  mgpf  14421  dfrhm2  14569  rhmex  14572  isdomn  14686  rmodislmod  14796  lidlmex  14920  mopnset  14997  cnfldstr  15003  cnfldcj  15010  cnfld0  15016  cnfldplusf  15019  zringcrng  15035  zringmulr  15042  zringmpg  15049  znval  15079  psrval  15160  fnpsr  15161  psrbagmaxlem1  15178  fnmpl  15225  txtopi  15504  txunii  15507  upxp  15515  uptx  15517  cnmpt1st  15531  cnmpt2nd  15532  txswaphmeolem  15563  qtopbasss  15764  cnmet  15773  cnfldms  15779  cnopncntop  15787  cnopn  15788  remet  15791  blssioo  15796  tgqioo  15798  tgioo2cntop  15800  tgioo2  15802  divcnap  15808  abscncf  15828  recncf  15829  imcncf  15830  cjcncf  15831  mulc1cncf  15832  cncfcn1cntop  15837  idcncf  15844  cdivcncfap  15847  expcncf  15852  cnrehmeocntop  15853  maxcncf  15858  mincncf  15859  ivthreinc  15888  hovercncf  15889  limccnp2lem  15919  limccnp2cntop  15920  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvrecap  15956  dveflem  15969  dvef  15970  sincn  16012  coscn  16013  reeff1oleme  16015  reeff1o  16016  cosz12  16024  sin0pilem1  16025  sin0pilem2  16026  pipos  16032  sinhalfpilem  16035  sincosq1lem  16069  sincosq1sgn  16070  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  cosq14gt0  16076  cosq23lt0  16077  coseq0q4123  16078  coseq00topi  16079  coseq0negpitopi  16080  tangtx  16082  sincos4thpi  16084  tan4thpi  16085  sincos6thpi  16086  pigt3  16088  cosordlem  16094  cosq34lt1  16095  cos02pilt1  16096  cos0pilt1  16097  ioocosf1o  16099  negpitopissre  16100  log1  16112  loge  16113  2logb9irr  16224  sqrt2cxp2logb9e3  16228  2logb9irrap  16230  log2tlbndlog2  16237  log2ublem1  16238  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  birthdaylog2  16245  ppi1  16287  cht1  16288  ppi1i  16289  ppi2i  16290  cht2  16293  cht3  16294  chtqrpcl  16296  mpodvdsmulf1o  16301  fsumdvdsmul  16302  1sgm2ppw  16306  ppiublem1  16308  ppiublem2  16309  ppiqub  16310  chtqub  16313  bpos1lem  16326  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsdir2lem2  16370  lgsdir2lem3  16371  lgseisenlem4  16414  2lgsoddprmlem3  16452  2sqlem9  16465  2sqlem10  16466  opvtxfvi  16490  opiedgfvi  16491  umgrbien  16573  usgrprc  16715  vtxdfifiun  16760  upgr2wlkdc  16840  konigsbergvtx  16945  konigsbergiedg  16946  konigsbergumgr  16950  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  konigsberg  16956  ex-fl  16961  ex-ceil  16962  ex-bc  16965  ex-dvds  16966  ex-gcd  16967  bj-charfunbi  17059  bj-unex  17167  bj-nn0suc0  17198  bj-nntrans  17199  bj-nnelirr  17201  012of  17245  2o01f  17246  pwle2  17250  nnsf  17271  peano3nninf  17273  exmidsbthrlem  17290  sbthom  17294  repiecelem  17297  repiecele0  17298  repiecege0  17299  isomninnlem  17302  iooref1o  17306  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  apdiff  17321  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  dceqnconst  17334  dcapnconst  17335  nconstwlpolemgt0  17338  taupi  17347