Theorem mp2an 426

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 424	. 2 |- ( ps -> ch )
5	1, 4	ax-mp 5	1 |- 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:  mp4an  427  jaoi  717  mp3an  1349  barbara  2151  eqeq12i  2218  vtocl2  2827  spc2ev  2868  sbc2ie  3069  csbieb  3134  sseq12i  3220  uneq12i  3324  ineq12i  3371  ifssun  3584  nelpri  3656  ralpr  3687  rexpr  3688  preq12i  3714  dfop  3817  opeq12i  3823  breq12i  4052  mpteq2ia  4129  exmidundif  4249  exmidundifim  4250  opex  4272  opi2  4276  opth2  4283  opeqsn  4296  opeqpr  4297  uniop  4299  opelopaba  4311  braba  4312  opelopab  4317  brab  4318  opelopabaf  4319  unex  4487  snnex  4494  op1stb  4524  ifelpwun  4529  ifex  4532  onun2i  4538  onsucssi  4553  ontriexmidim  4569  ontr2exmid  4572  onsucsssucexmid  4574  onsucelsucexmid  4577  opthreg  4603  tfis  4630  finds  4647  finds2  4648  nnregexmid  4668  xpeq12i  4696  opelvv  4724  eqrelriiv  4768  eqrelrdv  4770  xpss  4782  xpex  4789  relop  4827  brco  4848  opelcnv  4859  brcnv  4860  asymref  5067  codir  5070  ssrnres  5124  dmprop  5156  dfco2  5181  cossxp  5204  cocnvss  5207  coex  5227  funsn  5321  fnsn  5327  feq23i  5419  resasplitss  5454  fabex  5463  fvex  5595  xpsn  5755  fmptap  5773  opabex  5807  acexmidlemv  5941  oveq12i  5955  oprabid  5975  oprabss  6030  caovcom  6103  opabex3  6206  iunex  6207  oprabex  6212  ofmres  6220  op1st  6231  op2nd  6232  fo1st  6242  fo2nd  6243  mpoex  6299  1stconst  6306  2ndconst  6307  algrflem  6314  dftpos4  6348  tpostpos  6349  tpossym  6361  frecex  6479  frecfnom  6486  sucinc  6530  fnoei  6537  oeiexg  6538  nnacli  6567  nnmcli  6568  elec  6660  ecovcom  6728  ecovass  6730  ecovdi  6732  fnmap  6741  mapval  6746  elmap  6763  elpm  6765  elpm2  6766  map0  6775  ixpconst  6794  entri  6877  endisj  6918  xpcomco  6920  phplem2  6949  ssfiexmid  6972  domfiexmid  6974  exmidpw2en  7008  unfiexmid  7014  unfiin  7022  inresflem  7161  casefun  7186  caserel  7188  caseinj  7190  omp1eomlem  7195  omp1eom  7196  endjusym  7197  djufun  7205  djuinj  7207  ctssdccl  7212  ctssdclemr  7213  nninfex  7222  infnninf  7225  fodjuomnilemdc  7245  ctssexmid  7251  exmidonfinlem  7300  dju1p1e2  7304  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  exmidaclem  7319  pw1dom2  7338  onntri35  7348  onntri45  7352  2oneel  7367  2omotaplemst  7369  acnccim  7383  1lt2pi  7452  indpi  7454  1nq  7478  rec1nq  7507  1lt2nq  7518  ltaddnq  7519  halfnqq  7522  prarloclemarch2  7531  prarloclemlt  7605  prarloclemcalc  7614  genpelxp  7623  ltexprlempr  7720  recexprlempr  7744  cauappcvgprlemcl  7765  cauappcvgprlemladd  7770  caucvgprlemcl  7788  caucvgprprlemcl  7816  suplocexprlemell  7825  suplocexprlemdisj  7832  suplocexprlemub  7835  0r  7862  1sr  7863  m1r  7864  m1p1sr  7872  m1m1sr  7873  0lt1sr  7877  1ne0sr  7878  1idsr  7880  recexgt0sr  7885  prsradd  7898  caucvgsrlemoffres  7912  caucvgsr  7914  mappsrprg  7916  map2psrprg  7917  pitonnlem1p1  7958  pitonnlem2  7959  pitoregt0  7961  peano2nnnn  7965  axi2m1  7987  axprecex  7992  axcnre  7993  nnindnn  8005  nntopi  8006  0cn  8063  addcli  8075  mulcli  8076  mulcomi  8077  readdcli  8084  remulcli  8085  rexpssxrxp  8116  ltrelxr  8132  gtneii  8167  lttri3i  8169  letri3i  8170  ltnsymi  8171  lenlti  8172  ltlei  8173  mulgt0i  8181  mulgt0ii  8182  0lt1  8198  addcomi  8215  pncan3oi  8287  resubcli  8334  subcli  8347  pncan3i  8348  negsubi  8349  subnegi  8350  subeq0i  8351  neg11i  8352  negcon1i  8353  negcon2i  8354  mulneg1i  8475  mulneg2i  8476  mul2negi  8477  addgt0ii  8563  ltnegi  8565  lenegi  8566  ltnegcon2i  8567  lesub0i  8568  ltaddposi  8569  posdifi  8570  ltnegcon1i  8571  lenegcon1i  8572  subge0i  8573  1ap0  8662  ltapii  8707  recrecapi  8816  dividapi  8817  div0api  8818  rec11apii  8833  divdiv32api  8839  recgt0ii  8979  ltrecii  8990  ltdiv23ii  8999  sup3exmid  9029  nnssre  9039  nnind  9051  nnmulcli  9057  nnsubi  9075  0le2  9125  1lt3  9207  2lt4  9209  1lt4  9210  3lt5  9212  2lt5  9213  1lt5  9214  4lt6  9216  3lt6  9217  2lt6  9218  1lt6  9219  5lt7  9221  4lt7  9222  3lt7  9223  2lt7  9224  1lt7  9225  6lt8  9227  5lt8  9228  4lt8  9229  3lt8  9230  2lt8  9231  1lt8  9232  7lt9  9234  6lt9  9235  5lt9  9236  4lt9  9237  3lt9  9238  2lt9  9239  1lt9  9240  2muline0  9261  nn0addcli  9331  nn0mulcli  9332  nn0addge1i  9342  nn0addge2i  9343  dfz2  9444  halfnz  9468  9p1e10  9505  numnncl  9512  numltc  9528  le9lt10  9529  nummac  9547  8lt10  9634  7lt10  9635  6lt10  9636  5lt10  9637  4lt10  9638  3lt10  9639  2lt10  9640  1lt10  9641  eluzaddi  9674  eluzsubi  9675  eluz2nn  9686  eluz4eluz2  9687  uzuzle23  9691  eluzge3nn  9692  divfnzn  9741  elq  9742  qreccl  9762  xrltnr  9900  mnfltpnf  9906  xaddmnf1  9969  pnfaddmnf  9971  mnfaddpnf  9972  xrex  9977  xaddid1  9983  xsubge0  10002  xposdif  10003  xleaddadd  10008  elicc2i  10060  ioomax  10069  iccmax  10070  ioopos  10071  elxrge0  10099  iccshftri  10116  iccshftli  10118  iccdili  10120  icccntri  10122  unitssre  10126  fz10  10167  fzpreddisj  10192  fz0to4untppr  10245  dfrp2  10404  fldiv4p1lem1div2  10446  fldiv4lem1div2  10448  frecfzennn  10569  xnn0nnen  10580  fnn0nninf  10581  fxnn0nninf  10582  0tonninf  10583  1tonninf  10584  m1expcl2  10704  m1expcl  10705  nn0expcli  10708  sqmuli  10765  cu2  10781  i3  10784  subsqi  10792  binom2subi  10798  bcpasc  10909  4bc2eq6  10917  hashinfom  10921  prhash2ex  10952  hashp1i  10953  lsw0g  11040  rei  11152  imi  11153  readdi  11181  imaddi  11182  remuli  11183  immuli  11184  cjaddi  11185  cjmuli  11186  ipcni  11187  crrei  11189  crimi  11190  rexfiuz  11242  sqrt1  11299  sqrt4  11300  sqrt9  11301  abs1  11325  sqrtmulii  11387  abslti  11391  abslei  11392  abssubi  11403  absmuli  11404  sqabsaddi  11405  sqabssubi  11406  abstrii  11408  fimaxre2  11480  climz  11545  abscn2  11568  recn2  11570  imcn2  11571  climabs  11573  climre  11575  climim  11576  fsumcnv  11690  fsumrelem  11724  fsumre  11725  fsumim  11726  arisum2  11752  expcnv  11757  geo2sum2  11768  geo2lim  11769  0.999...  11774  geoihalfsum  11775  fprodcnv  11878  fprodge0  11890  fprodge1  11892  ege2le3  11924  ef0  11925  reeff1  11953  tan0  11984  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  cos1bnd  12012  cos2bnd  12013  sinltxirr  12014  sin01gt0  12015  cos01gt0  12016  sin02gt0  12017  sincos1sgn  12018  sincos2sgn  12019  cos12dec  12021  egt2lt3  12033  epos  12034  ene1  12038  eap1  12039  3dvds  12117  3dvdsdec  12118  3dvds2dec  12119  odd2np1lem  12125  n2dvds1  12165  z4even  12169  ndvdsi  12186  flodddiv4  12189  bitsp1o  12206  0bits  12212  gcd0val  12223  6gcd4e2  12258  3lcm2e6woprm  12350  6lcm4e12  12351  3lcm2e6  12424  sqrt2irrlem  12425  phimullem  12489  pockthi  12623  4sqlem19  12674  dec2dvds  12676  dec5dvds2  12678  dec2nprm  12680  modxai  12681  gcdi  12685  gcdmodi  12686  numexpp1  12689  karatsuba  12695  2exp7  12699  xpnnen  12707  xpomen  12708  ennnfonelemj0  12714  ennnfonelem0  12718  ennnfonelemhf1o  12726  exmidunben  12739  qnnen  12744  unct  12755  setscom  12814  strleun  12878  prdsex  13043  prdsvallem  13046  imasival  13080  ismgm  13131  fn0g  13149  fngsum  13162  issgrp  13177  ismnddef  13192  isghm  13521  isrng  13638  rngmgpf  13641  isring  13704  mgpf  13715  dfrhm2  13858  rhmex  13861  isdomn  13973  rmodislmod  14055  lidlmex  14179  mopnset  14256  cnfldstr  14262  cnfldcj  14269  cnfld0  14275  cnfldplusf  14278  zringcrng  14296  zringmulr  14303  zringmpg  14310  znval  14340  psrval  14370  fnpsr  14371  fnmpl  14397  txtopi  14675  txunii  14678  upxp  14686  uptx  14688  cnmpt1st  14702  cnmpt2nd  14703  txswaphmeolem  14734  qtopbasss  14935  cnmet  14944  cnfldms  14950  cnopncntop  14958  cnopn  14959  remet  14962  blssioo  14967  tgqioo  14969  tgioo2cntop  14971  tgioo2  14973  divcnap  14979  abscncf  14999  recncf  15000  imcncf  15001  cjcncf  15002  mulc1cncf  15003  cncfcn1cntop  15008  idcncf  15015  cdivcncfap  15018  expcncf  15023  cnrehmeocntop  15024  maxcncf  15029  mincncf  15030  ivthreinc  15059  hovercncf  15060  limccnp2lem  15090  limccnp2cntop  15091  dvcnp2cntop  15113  dvaddxxbr  15115  dvmulxxbr  15116  dvcoapbr  15121  dvrecap  15127  dveflem  15140  dvef  15141  sincn  15183  coscn  15184  reeff1oleme  15186  reeff1o  15187  cosz12  15194  sin0pilem1  15195  sin0pilem2  15196  pipos  15202  sinhalfpilem  15205  sincosq1lem  15239  sincosq1sgn  15240  sincosq2sgn  15241  sincosq3sgn  15242  sincosq4sgn  15243  sinq12gt0  15244  cosq14gt0  15246  cosq23lt0  15247  coseq0q4123  15248  coseq00topi  15249  coseq0negpitopi  15250  tangtx  15252  sincos4thpi  15254  tan4thpi  15255  sincos6thpi  15256  pigt3  15258  cosordlem  15263  cosq34lt1  15264  cos02pilt1  15265  cos0pilt1  15266  ioocosf1o  15268  negpitopissre  15269  log1  15280  loge  15281  2logb9irr  15385  sqrt2cxp2logb9e3  15389  2logb9irrap  15391  mpodvdsmulf1o  15404  fsumdvdsmul  15405  1sgm2ppw  15409  lgsdir2lem2  15448  lgsdir2lem3  15449  lgseisenlem4  15492  2lgsoddprmlem3  15530  2sqlem9  15543  2sqlem10  15544  opvtxfvi  15566  opiedgfvi  15567  ex-fl  15594  ex-ceil  15595  ex-bc  15598  ex-dvds  15599  ex-gcd  15600  bj-charfunbi  15680  bj-unex  15788  bj-nn0suc0  15819  bj-nntrans  15820  bj-nnelirr  15822  012of  15863  2o01f  15864  pwle2  15868  nnsf  15875  peano3nninf  15877  exmidsbthrlem  15894  sbthom  15898  isomninnlem  15902  iooref1o  15906  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  apdiff  15920  iswomninnlem  15921  iswomni0  15923  ismkvnnlem  15924  dceqnconst  15932  dcapnconst  15933  nconstwlpolemgt0  15936  taupi  15945