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  721  mp3an  1371  barbara  2176  eqeq12i  2243  el2v  2806  vtocl2  2857  spc2ev  2900  sbc2ie  3101  csbieb  3167  sseq12i  3253  uneq12i  3357  ineq12i  3404  ifssun  3618  nelpri  3691  ralpr  3722  rexpr  3723  preq12i  3751  dfop  3859  opeq12i  3865  breq12i  4095  mpteq2ia  4173  exmidundif  4294  exmidundifim  4295  opex  4319  opi2  4323  opth2  4330  opeqsn  4343  opeqpr  4344  uniop  4346  opelopaba  4358  braba  4359  opelopab  4364  brab  4365  opelopabaf  4366  unex  4536  snnex  4543  op1stb  4573  ifelpwun  4578  ifex  4581  onun2i  4587  onsucssi  4602  ontriexmidim  4618  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  opthreg  4652  tfis  4679  finds  4696  finds2  4697  nnregexmid  4717  xpeq12i  4745  opelvv  4774  eqrelriiv  4818  eqrelrdv  4820  xpss  4832  xpex  4840  relop  4878  brco  4899  opelcnv  4910  brcnv  4911  asymref  5120  codir  5123  ssrnres  5177  dmprop  5209  dfco2  5234  cossxp  5257  cocnvss  5260  coex  5280  funsn  5375  fnsn  5381  feq23i  5474  resasplitss  5513  fabex  5522  fvex  5655  xpsn  5819  fmptap  5839  opabex  5873  acexmidlemv  6011  oveq12i  6025  oprabid  6045  oprabss  6102  caovcom  6175  opabex3  6279  iunex  6280  oprabex  6285  ofmres  6293  op1st  6304  op2nd  6305  fo1st  6315  fo2nd  6316  mpoex  6374  1stconst  6381  2ndconst  6382  algrflem  6389  dftpos4  6424  tpostpos  6425  tpossym  6437  frecex  6555  frecfnom  6562  2oex  6594  sucinc  6608  fnoei  6615  oeiexg  6616  nnacli  6645  nnmcli  6646  elec  6738  ecovcom  6806  ecovass  6808  ecovdi  6810  fnmap  6819  mapval  6824  elmap  6841  elpm  6843  elpm2  6844  map0  6853  ixpconst  6872  entri  6955  endisj  7003  xpcomco  7005  phplem2  7034  1ndom2  7046  ssfiexmid  7058  domfiexmid  7060  exmidpw2en  7097  unfiexmid  7103  unfiin  7111  inresflem  7250  casefun  7275  caserel  7277  caseinj  7279  omp1eomlem  7284  omp1eom  7285  endjusym  7286  djufun  7294  djuinj  7296  ctssdccl  7301  ctssdclemr  7302  nninfex  7311  infnninf  7314  fodjuomnilemdc  7334  ctssexmid  7340  exmidonfinlem  7394  dju1p1e2  7398  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  pw1dom2  7435  onntri35  7445  onntri45  7449  2oneel  7465  2omotaplemst  7467  acnccim  7481  1lt2pi  7550  indpi  7552  1nq  7576  rec1nq  7605  1lt2nq  7616  ltaddnq  7617  halfnqq  7620  prarloclemarch2  7629  prarloclemlt  7703  prarloclemcalc  7712  genpelxp  7721  ltexprlempr  7818  recexprlempr  7842  cauappcvgprlemcl  7863  cauappcvgprlemladd  7868  caucvgprlemcl  7886  caucvgprprlemcl  7914  suplocexprlemell  7923  suplocexprlemdisj  7930  suplocexprlemub  7933  0r  7960  1sr  7961  m1r  7962  m1p1sr  7970  m1m1sr  7971  0lt1sr  7975  1ne0sr  7976  1idsr  7978  recexgt0sr  7983  prsradd  7996  caucvgsrlemoffres  8010  caucvgsr  8012  mappsrprg  8014  map2psrprg  8015  pitonnlem1p1  8056  pitonnlem2  8057  pitoregt0  8059  peano2nnnn  8063  axi2m1  8085  axprecex  8090  axcnre  8091  nnindnn  8103  nntopi  8104  0cn  8161  addcli  8173  mulcli  8174  mulcomi  8175  readdcli  8182  remulcli  8183  rexpssxrxp  8214  ltrelxr  8230  gtneii  8265  lttri3i  8267  letri3i  8268  ltnsymi  8269  lenlti  8270  ltlei  8271  mulgt0i  8279  mulgt0ii  8280  0lt1  8296  addcomi  8313  pncan3oi  8385  resubcli  8432  subcli  8445  pncan3i  8446  negsubi  8447  subnegi  8448  subeq0i  8449  neg11i  8450  negcon1i  8451  negcon2i  8452  mulneg1i  8573  mulneg2i  8574  mul2negi  8575  addgt0ii  8661  ltnegi  8663  lenegi  8664  ltnegcon2i  8665  lesub0i  8666  ltaddposi  8667  posdifi  8668  ltnegcon1i  8669  lenegcon1i  8670  subge0i  8671  1ap0  8760  ltapii  8805  recrecapi  8914  dividapi  8915  div0api  8916  rec11apii  8931  divdiv32api  8937  recgt0ii  9077  ltrecii  9088  ltdiv23ii  9097  sup3exmid  9127  nnssre  9137  nnind  9149  nnmulcli  9155  nnsubi  9173  0le2  9223  1lt3  9305  2lt4  9307  1lt4  9308  3lt5  9310  2lt5  9311  1lt5  9312  4lt6  9314  3lt6  9315  2lt6  9316  1lt6  9317  5lt7  9319  4lt7  9320  3lt7  9321  2lt7  9322  1lt7  9323  6lt8  9325  5lt8  9326  4lt8  9327  3lt8  9328  2lt8  9329  1lt8  9330  7lt9  9332  6lt9  9333  5lt9  9334  4lt9  9335  3lt9  9336  2lt9  9337  1lt9  9338  2muline0  9359  nn0addcli  9429  nn0mulcli  9430  nn0addge1i  9440  nn0addge2i  9441  dfz2  9542  halfnz  9566  9p1e10  9603  numnncl  9610  numltc  9626  le9lt10  9627  nummac  9645  8lt10  9732  7lt10  9733  6lt10  9734  5lt10  9735  4lt10  9736  3lt10  9737  2lt10  9738  1lt10  9739  eluzaddi  9773  eluzsubi  9774  uzuzle23  9786  uzuzle24  9787  uzuzle34  9788  eluz2nn  9790  eluz4eluz2  9792  eluzge3nn  9796  divfnzn  9845  elq  9846  qreccl  9866  xrltnr  10004  mnfltpnf  10010  xaddmnf1  10073  pnfaddmnf  10075  mnfaddpnf  10076  xrex  10081  xaddid1  10087  xsubge0  10106  xposdif  10107  xleaddadd  10112  elicc2i  10164  ioomax  10173  iccmax  10174  ioopos  10175  elxrge0  10203  iccshftri  10220  iccshftli  10222  iccdili  10224  icccntri  10226  unitssre  10230  fz10  10271  fzpreddisj  10296  fz0to4untppr  10349  dfrp2  10513  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  frecfzennn  10678  xnn0nnen  10689  fnn0nninf  10690  fxnn0nninf  10691  0tonninf  10692  1tonninf  10693  m1expcl2  10813  m1expcl  10814  nn0expcli  10817  sqmuli  10874  cu2  10890  i3  10893  subsqi  10901  binom2subi  10907  bcpasc  11018  4bc2eq6  11026  hashinfom  11030  prhash2ex  11063  hashp1i  11064  lsw0g  11152  swrdccat3blem  11310  rei  11450  imi  11451  readdi  11479  imaddi  11480  remuli  11481  immuli  11482  cjaddi  11483  cjmuli  11484  ipcni  11485  crrei  11487  crimi  11488  rexfiuz  11540  sqrt1  11597  sqrt4  11598  sqrt9  11599  abs1  11623  sqrtmulii  11685  abslti  11689  abslei  11690  abssubi  11701  absmuli  11702  sqabsaddi  11703  sqabssubi  11704  abstrii  11706  fimaxre2  11778  climz  11843  abscn2  11866  recn2  11868  imcn2  11869  climabs  11871  climre  11873  climim  11874  fsumcnv  11988  fsumrelem  12022  fsumre  12023  fsumim  12024  arisum2  12050  expcnv  12055  geo2sum2  12066  geo2lim  12067  0.999...  12072  geoihalfsum  12073  fprodcnv  12176  fprodge0  12188  fprodge1  12190  ege2le3  12222  ef0  12223  reeff1  12251  tan0  12282  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos1bnd  12310  cos2bnd  12311  sinltxirr  12312  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  sincos1sgn  12316  sincos2sgn  12317  cos12dec  12319  egt2lt3  12331  epos  12332  ene1  12336  eap1  12337  3dvds  12415  3dvdsdec  12416  3dvds2dec  12417  odd2np1lem  12423  n2dvds1  12463  z4even  12467  ndvdsi  12484  flodddiv4  12487  bitsp1o  12504  0bits  12510  gcd0val  12521  6gcd4e2  12556  3lcm2e6woprm  12648  6lcm4e12  12649  3lcm2e6  12722  sqrt2irrlem  12723  phimullem  12787  pockthi  12921  4sqlem19  12972  dec2dvds  12974  dec5dvds2  12976  dec2nprm  12978  modxai  12979  gcdi  12983  gcdmodi  12984  numexpp1  12987  karatsuba  12993  2exp7  12997  xpnnen  13005  xpomen  13006  ennnfonelemj0  13012  ennnfonelem0  13016  ennnfonelemhf1o  13024  exmidunben  13037  qnnen  13042  unct  13053  setscom  13112  strleun  13177  prdsex  13342  prdsvallem  13345  imasival  13379  ismgm  13430  fn0g  13448  fngsum  13461  issgrp  13476  ismnddef  13491  isghm  13820  isrng  13937  rngmgpf  13940  isring  14003  mgpf  14014  dfrhm2  14158  rhmex  14161  isdomn  14273  rmodislmod  14355  lidlmex  14479  mopnset  14556  cnfldstr  14562  cnfldcj  14569  cnfld0  14575  cnfldplusf  14578  zringcrng  14596  zringmulr  14603  zringmpg  14610  znval  14640  psrval  14670  fnpsr  14671  fnmpl  14697  txtopi  14975  txunii  14978  upxp  14986  uptx  14988  cnmpt1st  15002  cnmpt2nd  15003  txswaphmeolem  15034  qtopbasss  15235  cnmet  15244  cnfldms  15250  cnopncntop  15258  cnopn  15259  remet  15262  blssioo  15267  tgqioo  15269  tgioo2cntop  15271  tgioo2  15273  divcnap  15279  abscncf  15299  recncf  15300  imcncf  15301  cjcncf  15302  mulc1cncf  15303  cncfcn1cntop  15308  idcncf  15315  cdivcncfap  15318  expcncf  15323  cnrehmeocntop  15324  maxcncf  15329  mincncf  15330  ivthreinc  15359  hovercncf  15360  limccnp2lem  15390  limccnp2cntop  15391  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvrecap  15427  dveflem  15440  dvef  15441  sincn  15483  coscn  15484  reeff1oleme  15486  reeff1o  15487  cosz12  15494  sin0pilem1  15495  sin0pilem2  15496  pipos  15502  sinhalfpilem  15505  sincosq1lem  15539  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  cosq14gt0  15546  cosq23lt0  15547  coseq0q4123  15548  coseq00topi  15549  coseq0negpitopi  15550  tangtx  15552  sincos4thpi  15554  tan4thpi  15555  sincos6thpi  15556  pigt3  15558  cosordlem  15563  cosq34lt1  15564  cos02pilt1  15565  cos0pilt1  15566  ioocosf1o  15568  negpitopissre  15569  log1  15580  loge  15581  2logb9irr  15685  sqrt2cxp2logb9e3  15689  2logb9irrap  15691  mpodvdsmulf1o  15704  fsumdvdsmul  15705  1sgm2ppw  15709  lgsdir2lem2  15748  lgsdir2lem3  15749  lgseisenlem4  15792  2lgsoddprmlem3  15830  2sqlem9  15843  2sqlem10  15844  opvtxfvi  15868  opiedgfvi  15869  umgrbien  15951  usgrprc  16091  vtxdfifiun  16103  upgr2wlkdc  16172  ex-fl  16257  ex-ceil  16258  ex-bc  16261  ex-dvds  16262  ex-gcd  16263  bj-charfunbi  16342  bj-unex  16450  bj-nn0suc0  16481  bj-nntrans  16482  bj-nnelirr  16484  012of  16528  2o01f  16529  pwle2  16535  nnsf  16543  peano3nninf  16545  exmidsbthrlem  16562  sbthom  16566  isomninnlem  16570  iooref1o  16574  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  apdiff  16588  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  dceqnconst  16600  dcapnconst  16601  nconstwlpolemgt0  16604  taupi  16613