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  724  mp3an  1374  barbara  2181  eqeq12i  2248  el2v  2821  vtocl2  2872  spc2ev  2915  sbc2ie  3117  csbieb  3183  sseq12i  3270  uneq12i  3375  ineq12i  3424  ifssun  3641  nelpri  3718  ralpr  3749  rexpr  3750  preq12i  3778  dfop  3887  opeq12i  3893  breq12i  4123  mpteq2ia  4201  exmidundif  4324  exmidundifim  4325  opex  4350  opi2  4354  opth2  4361  opeqsn  4374  opeqpr  4375  uniop  4377  opelopaba  4389  braba  4390  opelopab  4395  brab  4396  opelopabaf  4397  unex  4567  snnex  4574  op1stb  4604  ifelpwun  4609  ifex  4612  onun2i  4618  onsucssi  4633  ontriexmidim  4649  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  opthreg  4683  tfis  4710  finds  4727  finds2  4728  nnregexmid  4748  xpeq12i  4776  opelvv  4805  eqrelriiv  4849  eqrelrdv  4851  xpss  4863  xpex  4871  relop  4910  brco  4931  opelcnv  4942  brcnv  4943  asymref  5153  codir  5156  ssrnres  5210  dmprop  5242  dfco2  5267  cossxp  5290  cocnvss  5293  coex  5313  funsn  5409  fnsn  5415  feq23i  5508  resasplitss  5549  fabex  5560  fvex  5695  xpsn  5859  fmptap  5879  opabex  5915  rinvf1o  6008  acexmidlemv  6056  oveq12i  6070  oprabid  6090  oprabss  6147  caovcom  6220  opabex3  6324  iunex  6325  oprabex  6334  ofmres  6342  op1st  6353  op2nd  6354  fo1st  6364  fo2nd  6365  mpoex  6423  1stconst  6430  2ndconst  6431  algrflem  6438  dftpos4  6507  tpostpos  6508  tpossym  6520  frecex  6638  frecfnom  6645  2oex  6677  sucinc  6691  fnoei  6698  oeiexg  6699  nnacli  6728  nnmcli  6729  elec  6821  ecovcom  6889  ecovass  6891  ecovdi  6893  fnmap  6902  mapval  6907  elmap  6924  elpm  6926  elpm2  6927  map0  6937  ixpconst  6956  entri  7039  endisj  7088  xpcomco  7090  phplem2  7120  1ndom2  7132  ssfiexmid  7144  domfiexmid  7148  exmidpw2en  7185  unfiexmid  7191  unfiin  7199  inresflem  7364  casefun  7389  caserel  7391  caseinj  7393  omp1eomlem  7398  omp1eom  7399  endjusym  7400  djufun  7408  djuinj  7410  ctssdccl  7415  ctssdclemr  7416  nninfex  7425  infnninf  7428  fodjuomnilemdc  7448  ctssexmid  7454  exmidonfinlem  7509  dju1p1e2  7513  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  pw1dom2  7550  onntri35  7560  onntri45  7564  2oneel  7586  2omotaplemst  7588  acnccim  7602  1lt2pi  7671  indpi  7673  1nq  7697  rec1nq  7726  1lt2nq  7737  ltaddnq  7738  halfnqq  7741  prarloclemarch2  7750  prarloclemlt  7824  prarloclemcalc  7833  genpelxp  7842  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  cauappcvgprlemladd  7989  caucvgprlemcl  8007  caucvgprprlemcl  8035  suplocexprlemell  8044  suplocexprlemdisj  8051  suplocexprlemub  8054  0r  8081  1sr  8082  m1r  8083  m1p1sr  8091  m1m1sr  8092  0lt1sr  8096  1ne0sr  8097  1idsr  8099  recexgt0sr  8104  prsradd  8117  caucvgsrlemoffres  8131  caucvgsr  8133  mappsrprg  8135  map2psrprg  8136  pitonnlem1p1  8177  pitonnlem2  8178  pitoregt0  8180  peano2nnnn  8184  axi2m1  8206  axprecex  8211  axcnre  8212  nnindnn  8224  nntopi  8225  0cn  8282  addcli  8294  mulcli  8295  mulcomi  8296  readdcli  8303  remulcli  8304  rexpssxrxp  8334  ltrelxr  8350  gtneii  8385  lttri3i  8387  letri3i  8388  ltnsymi  8389  lenlti  8390  ltlei  8391  mulgt0i  8399  mulgt0ii  8400  0lt1  8416  addcomi  8433  pncan3oi  8505  resubcli  8552  subcli  8565  pncan3i  8566  negsubi  8567  subnegi  8568  subeq0i  8569  neg11i  8570  negcon1i  8571  negcon2i  8572  mulneg1i  8694  mulneg2i  8695  mul2negi  8696  addgt0ii  8782  ltnegi  8784  lenegi  8785  ltnegcon2i  8786  lesub0i  8787  ltaddposi  8788  posdifi  8789  ltnegcon1i  8790  lenegcon1i  8791  subge0i  8792  1ap0  8881  ltapii  8926  recrecapi  9035  dividapi  9036  div0api  9037  rec11apii  9052  divdiv32api  9058  recgt0ii  9198  ltrecii  9209  ltdiv23ii  9218  sup3exmid  9248  nnssre  9258  nnind  9270  nnmulcli  9276  nnsubi  9294  0le2  9344  1lt3  9426  2lt4  9428  1lt4  9429  3lt5  9431  2lt5  9432  1lt5  9433  4lt6  9435  3lt6  9436  2lt6  9437  1lt6  9438  5lt7  9440  4lt7  9441  3lt7  9442  2lt7  9443  1lt7  9444  6lt8  9446  5lt8  9447  4lt8  9448  3lt8  9449  2lt8  9450  1lt8  9451  7lt9  9453  6lt9  9454  5lt9  9455  4lt9  9456  3lt9  9457  2lt9  9458  1lt9  9459  2muline0  9480  nn0addcli  9550  nn0mulcli  9551  nn0addge1i  9561  nn0addge2i  9562  dfz2  9667  halfnz  9692  9p1e10  9729  numnncl  9736  numltc  9752  le9lt10  9753  nummac  9771  8lt10  9858  7lt10  9859  6lt10  9860  5lt10  9861  4lt10  9862  3lt10  9863  2lt10  9864  1lt10  9865  eluzaddi  9899  eluzsubi  9900  uzuzle23  9912  uzuzle24  9913  uzuzle34  9914  eluz2nn  9916  eluz4eluz2  9918  eluzge3nn  9922  divfnzn  9971  elq  9972  qreccl  9992  xrltnr  10131  mnfltpnf  10137  xaddmnf1  10200  pnfaddmnf  10202  mnfaddpnf  10203  xrex  10208  xaddid1  10214  xsubge0  10233  xposdif  10234  xleaddadd  10239  elicc2i  10291  ioomax  10300  iccmax  10301  ioopos  10302  elxrge0  10330  iccshftri  10347  iccshftli  10349  iccdili  10351  icccntri  10353  unitssre  10358  fz10  10400  fzpreddisj  10427  fz0to4untppr  10480  dfrp2  10647  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  frecfzennn  10812  xnn0nnen  10823  fnn0nninf  10824  fxnn0nninf  10825  0tonninf  10826  1tonninf  10827  m1expcl2  10947  m1expcl  10948  nn0expcli  10951  sqmuli  11008  cu2  11024  i3  11027  subsqi  11035  binom2subi  11041  bcpasc  11153  4bc2eq6  11162  hashinfom  11166  prhash2ex  11199  hashp1i  11200  lsw0g  11298  swrdccat3blem  11456  rei  11609  imi  11610  readdi  11638  imaddi  11639  remuli  11640  immuli  11641  cjaddi  11642  cjmuli  11643  ipcni  11644  crrei  11646  crimi  11647  rexfiuz  11699  sqrt1  11756  sqrt4  11757  sqrt9  11758  abs1  11782  sqrtmulii  11844  abslti  11848  abslei  11849  abssubi  11860  absmuli  11861  sqabsaddi  11862  sqabssubi  11863  abstrii  11865  fimaxre2  11937  climz  12002  abscn2  12025  recn2  12027  imcn2  12028  climabs  12030  climre  12032  climim  12033  fsumcnv  12148  fsumrelem  12182  fsumre  12183  fsumim  12184  arisum2  12210  expcnv  12215  geo2sum2  12226  geo2lim  12227  0.999...  12232  geoihalfsum  12233  fprodcnv  12336  fprodge0  12348  fprodge1  12350  ege2le3  12382  ef0  12383  reeff1  12411  tan0  12442  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos1bnd  12470  cos2bnd  12471  sinltxirr  12472  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  sincos1sgn  12476  sincos2sgn  12477  cos12dec  12479  egt2lt3  12491  epos  12492  ene1  12496  eap1  12497  3dvds  12575  3dvdsdec  12576  3dvds2dec  12577  odd2np1lem  12583  n2dvds1  12623  z4even  12627  ndvdsi  12644  flodddiv4  12647  bitsp1o  12664  0bits  12670  gcd0val  12681  6gcd4e2  12716  3lcm2e6woprm  12808  6lcm4e12  12809  3lcm2e6  12882  sqrt2irrlem  12883  phimullem  12947  pockthi  13081  4sqlem19  13132  dec2dvds  13134  dec5dvds2  13136  dec2nprm  13138  modxai  13139  gcdi  13143  gcdmodi  13144  numexpp1  13147  karatsuba  13153  2exp7  13157  ballotfilemofi  13163  ballotfilem1  13164  ballotfilem2  13172  ballotfilemfmpn  13178  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilem4  13185  ballotfilemiex  13188  ballotfilemimin  13193  ballotfilemic  13194  ballotfilemsval  13196  ballotfilemsdom  13199  ballotfilemsel1i  13200  ballotfilemsima  13203  ballotfilemrval  13205  ballotfilemfrceq  13216  ballotfilemfrcn0  13217  ballotfilem1ri  13222  ballotfilem7  13223  ballotfilem8  13224  ballotfilemth  13225  xpnnen  13229  xpomen  13230  ennnfonelemj0  13236  ennnfonelem0  13240  ennnfonelemhf1o  13248  exmidunben  13261  qnnen  13266  unct  13277  setscom  13336  strleun  13401  prdsvallem  13564  imasival  13570  ismgm  13620  fn0g  13638  fngsum  13651  issgrp  13666  ismnddef  13679  isghm  13996  prdsex  14114  isrng  14173  rngmgpf  14176  isring  14243  mgpf  14254  dfrhm2  14399  rhmex  14402  isdomn  14516  rmodislmod  14625  lidlmex  14749  mopnset  14826  cnfldstr  14832  cnfldcj  14839  cnfld0  14845  cnfldplusf  14848  zringcrng  14866  zringmulr  14873  zringmpg  14880  znval  14910  psrval  14940  fnpsr  14941  fnmpl  14974  txtopi  15252  txunii  15255  upxp  15263  uptx  15265  cnmpt1st  15279  cnmpt2nd  15280  txswaphmeolem  15311  qtopbasss  15512  cnmet  15521  cnfldms  15527  cnopncntop  15535  cnopn  15536  remet  15539  blssioo  15544  tgqioo  15546  tgioo2cntop  15548  tgioo2  15550  divcnap  15556  abscncf  15576  recncf  15577  imcncf  15578  cjcncf  15579  mulc1cncf  15580  cncfcn1cntop  15585  idcncf  15592  cdivcncfap  15595  expcncf  15600  cnrehmeocntop  15601  maxcncf  15606  mincncf  15607  ivthreinc  15636  hovercncf  15637  limccnp2lem  15667  limccnp2cntop  15668  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvrecap  15704  dveflem  15717  dvef  15718  sincn  15760  coscn  15761  reeff1oleme  15763  reeff1o  15764  cosz12  15771  sin0pilem1  15772  sin0pilem2  15773  pipos  15779  sinhalfpilem  15782  sincosq1lem  15816  sincosq1sgn  15817  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  cosq14gt0  15823  cosq23lt0  15824  coseq0q4123  15825  coseq00topi  15826  coseq0negpitopi  15827  tangtx  15829  sincos4thpi  15831  tan4thpi  15832  sincos6thpi  15833  pigt3  15835  cosordlem  15840  cosq34lt1  15841  cos02pilt1  15842  cos0pilt1  15843  ioocosf1o  15845  negpitopissre  15846  log1  15857  loge  15858  2logb9irr  15962  sqrt2cxp2logb9e3  15966  2logb9irrap  15968  mpodvdsmulf1o  15984  fsumdvdsmul  15985  1sgm2ppw  15989  lgsdir2lem2  16028  lgsdir2lem3  16029  lgseisenlem4  16072  2lgsoddprmlem3  16110  2sqlem9  16123  2sqlem10  16124  opvtxfvi  16148  opiedgfvi  16149  umgrbien  16231  usgrprc  16373  vtxdfifiun  16418  upgr2wlkdc  16498  konigsbergvtx  16603  konigsbergiedg  16604  konigsbergumgr  16608  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613  konigsberg  16614  ex-fl  16619  ex-ceil  16620  ex-bc  16623  ex-dvds  16624  ex-gcd  16625  bj-charfunbi  16707  bj-unex  16815  bj-nn0suc0  16846  bj-nntrans  16847  bj-nnelirr  16849  012of  16893  2o01f  16894  pwle2  16898  nnsf  16909  peano3nninf  16911  exmidsbthrlem  16928  sbthom  16932  repiecelem  16935  repiecele0  16936  repiecege0  16937  isomninnlem  16940  iooref1o  16944  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  apdiff  16958  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963  dceqnconst  16972  dcapnconst  16973  nconstwlpolemgt0  16976  taupi  16985