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  6538  tpostpos  6539  tpossym  6551  frecex  6669  frecfnom  6676  2oex  6708  sucinc  6722  fnoei  6729  oeiexg  6730  nnacli  6759  nnmcli  6760  elec  6852  ecovcom  6920  ecovass  6922  ecovdi  6924  fnmap  6933  mapval  6938  elmap  6962  elpm  6964  elpm2  6965  map0  6975  ixpconst  6994  entri  7077  endisj  7126  xpcomco  7128  phplem2  7158  1ndom2  7170  ssfiexmid  7182  domfiexmid  7186  exmidpw2en  7223  unfiexmid  7229  unfiin  7237  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  9728  halfnz  9753  9p1e10  9790  numnncl  9797  numltc  9818  le9lt10  9819  nummac  9837  8lt10  9924  7lt10  9925  6lt10  9926  5lt10  9927  4lt10  9928  3lt10  9929  2lt10  9930  1lt10  9931  eluzaddi  9965  eluzsubi  9966  uzuzle23  9978  uzuzle24  9979  uzuzle34  9980  eluz2nn  9982  eluz4eluz2  9984  eluzge3nn  9988  divfnzn  10037  elq  10038  qreccl  10058  xrltnr  10198  mnfltpnf  10204  xaddmnf1  10267  pnfaddmnf  10269  mnfaddpnf  10270  xrex  10275  xaddid1  10281  xsubge0  10300  xposdif  10301  xleaddadd  10306  elicc2i  10358  ioomax  10367  iccmax  10368  ioopos  10369  elxrge0  10397  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  unitssre  10425  fz10  10467  fz00m1  10468  fzpreddisj  10495  fz0to4untppr  10548  dfrp2  10715  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  frecfzennn  10884  xnn0nnen  10895  fnn0nninf  10896  fxnn0nninf  10897  0tonninf  10898  1tonninf  10899  m1expcl2  11019  m1expcl  11020  nn0expcli  11023  sqmuli  11080  cu2  11096  i3  11099  subsqi  11107  binom2subi  11113  bcpasc  11226  4bc2eq6  11235  hashinfom  11239  prhash2ex  11272  hashp1i  11273  lsw0g  11375  swrdccat3blem  11533  rei  11687  imi  11688  readdi  11716  imaddi  11717  remuli  11718  immuli  11719  cjaddi  11720  cjmuli  11721  ipcni  11722  crrei  11724  crimi  11725  rexfiuz  11777  sqrt1  11834  sqrt4  11835  sqrt9  11836  abs1  11860  sqrtmulii  11923  abslti  11927  abslei  11928  abssubi  11939  absmuli  11940  sqabsaddi  11941  sqabssubi  11942  abstrii  11944  fimaxre2  12016  fiidxsupcl  12018  climz  12083  abscn2  12106  recn2  12108  imcn2  12109  climabs  12111  climre  12113  climim  12114  fsumcnv  12229  fsumrelem  12263  fsumre  12264  fsumim  12265  arisum2  12291  expcnv  12296  geo2sum2  12307  geo2lim  12308  0.999...  12313  geoihalfsum  12314  fprodcnv  12417  fprodge0  12429  fprodge1  12431  ege2le3  12463  ef0  12464  reeff1  12492  tan0  12523  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  sinltxirr  12553  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  sincos1sgn  12557  sincos2sgn  12558  cos12dec  12560  egt2lt3  12572  epos  12573  ene1  12577  eap1  12578  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  odd2np1lem  12664  n2dvds1  12704  z4even  12708  ndvdsi  12725  flodddiv4  12728  bitsp1o  12745  0bits  12751  gcd0val  12762  6gcd4e2  12797  3lcm2e6woprm  12889  6lcm4e12  12890  3lcm2e6  12964  sqrt2irrlem  12965  phimullem  13032  pockthi  13166  4sqlem19  13217  dec2dvds  13219  dec5dvds2  13221  dec2nprm  13223  modxai  13224  mod2xnegi  13227  gcdi  13229  gcdmodi  13230  numexpp1  13233  karatsuba  13239  2exp7  13243  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilemofi  13277  ballotfilem1  13278  ballotfilem2  13286  ballotfilemfmpn  13292  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilem4  13299  ballotfilemiex  13302  ballotfilemimin  13307  ballotfilemic  13308  ballotfilemsval  13310  ballotfilemsdom  13313  ballotfilemsel1i  13314  ballotfilemsima  13317  ballotfilemrval  13319  ballotfilemfrceq  13330  ballotfilemfrcn0  13331  ballotfilem1ri  13336  ballotfilem7  13337  ballotfilem8  13338  ballotfilemth  13339  xpnnen  13343  xpomen  13344  ennnfonelemj0  13350  ennnfonelem0  13354  ennnfonelemhf1o  13362  exmidunben  13375  qnnen  13380  unct  13391  setscom  13450  strleun  13517  prdsvallem  13680  imasival  13686  ismgm  13736  fn0g  13754  fngzsum  13767  issgrp  13777  ismnddef  13790  isghm  14105  prdsex  14279  isrng  14340  rngmgpf  14343  isring  14411  mgpf  14422  dfrhm2  14570  rhmex  14573  isdomn  14687  rmodislmod  14797  lidlmex  14921  mopnset  14998  cnfldstr  15004  cnfldcj  15011  cnfld0  15017  cnfldplusf  15020  zringcrng  15036  zringmulr  15043  zringmpg  15050  znval  15080  psrval  15159  fnpsr  15160  fnmpl  15209  txtopi  15487  txunii  15490  upxp  15498  uptx  15500  cnmpt1st  15514  cnmpt2nd  15515  txswaphmeolem  15546  qtopbasss  15747  cnmet  15756  cnfldms  15762  cnopncntop  15770  cnopn  15771  remet  15774  blssioo  15779  tgqioo  15781  tgioo2cntop  15783  tgioo2  15785  divcnap  15791  abscncf  15811  recncf  15812  imcncf  15813  cjcncf  15814  mulc1cncf  15815  cncfcn1cntop  15820  idcncf  15827  cdivcncfap  15830  expcncf  15835  cnrehmeocntop  15836  maxcncf  15841  mincncf  15842  ivthreinc  15871  hovercncf  15872  limccnp2lem  15902  limccnp2cntop  15903  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvrecap  15939  dveflem  15952  dvef  15953  sincn  15995  coscn  15996  reeff1oleme  15998  reeff1o  15999  cosz12  16007  sin0pilem1  16008  sin0pilem2  16009  pipos  16015  sinhalfpilem  16018  sincosq1lem  16052  sincosq1sgn  16053  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  cosq14gt0  16059  cosq23lt0  16060  coseq0q4123  16061  coseq00topi  16062  coseq0negpitopi  16063  tangtx  16065  sincos4thpi  16067  tan4thpi  16068  sincos6thpi  16069  pigt3  16071  cosordlem  16077  cosq34lt1  16078  cos02pilt1  16079  cos0pilt1  16080  ioocosf1o  16082  negpitopissre  16083  log1  16095  loge  16096  2logb9irr  16207  sqrt2cxp2logb9e3  16211  2logb9irrap  16213  log2tlbndlog2  16220  log2ublem1  16221  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  ppi1  16270  cht1  16271  ppi1i  16272  ppi2i  16273  cht2  16276  cht3  16277  chtqrpcl  16279  mpodvdsmulf1o  16284  fsumdvdsmul  16285  1sgm2ppw  16289  ppiublem1  16291  ppiublem2  16292  ppiqub  16293  chtqub  16296  bpos1lem  16309  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsdir2lem2  16353  lgsdir2lem3  16354  lgseisenlem4  16397  2lgsoddprmlem3  16435  2sqlem9  16448  2sqlem10  16449  opvtxfvi  16473  opiedgfvi  16474  umgrbien  16556  usgrprc  16698  vtxdfifiun  16743  upgr2wlkdc  16823  konigsbergvtx  16928  konigsbergiedg  16929  konigsbergumgr  16933  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem5  16938  konigsberg  16939  ex-fl  16944  ex-ceil  16945  ex-bc  16948  ex-dvds  16949  ex-gcd  16950  bj-charfunbi  17042  bj-unex  17150  bj-nn0suc0  17181  bj-nntrans  17182  bj-nnelirr  17184  012of  17228  2o01f  17229  pwle2  17233  nnsf  17254  peano3nninf  17256  exmidsbthrlem  17273  sbthom  17277  repiecelem  17280  repiecele0  17281  repiecege0  17282  isomninnlem  17285  iooref1o  17289  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  apdiff  17304  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  dceqnconst  17317  dcapnconst  17318  nconstwlpolemgt0  17321  taupi  17330