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  4139  mpteq2ia  4217  exmidundif  4343  exmidundifim  4344  opex  4369  opi2  4373  opth2  4380  opeqsn  4393  opeqpr  4394  uniop  4396  opelopaba  4408  braba  4409  opelopab  4414  brab  4415  opelopabaf  4416  unex  4587  snnex  4594  op1stb  4624  ifelpwun  4629  ifex  4632  onun2i  4638  onsucssi  4653  ontriexmidim  4669  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  opthreg  4703  tfis  4730  finds  4747  finds2  4748  nnregexmid  4768  xpeq12i  4796  opelvv  4825  eqrelriiv  4869  eqrelrdv  4871  xpss  4883  xpex  4891  relop  4930  brco  4951  opelcnv  4962  brcnv  4963  asymref  5173  codir  5176  ssrnres  5230  dmprop  5262  dfco2  5287  cossxp  5310  cocnvss  5313  coex  5333  funsn  5429  fnsn  5435  feq23i  5528  resasplitss  5569  fabex  5580  fvex  5715  xpsn  5885  fmptap  5905  opabex  5941  rinvf1o  6035  acexmidlemv  6083  oveq12i  6097  oprabid  6117  oprabss  6174  caovcom  6247  opabex3  6351  iunex  6352  oprabex  6361  ofmres  6369  op1st  6380  op2nd  6381  fo1st  6391  fo2nd  6392  mpoex  6450  1stconst  6457  2ndconst  6458  algrflem  6465  dftpos4  6534  tpostpos  6535  tpossym  6547  frecex  6665  frecfnom  6672  2oex  6704  sucinc  6718  fnoei  6725  oeiexg  6726  nnacli  6755  nnmcli  6756  elec  6848  ecovcom  6916  ecovass  6918  ecovdi  6920  fnmap  6929  mapval  6934  elmap  6958  elpm  6960  elpm2  6961  map0  6971  ixpconst  6990  entri  7073  endisj  7122  xpcomco  7124  phplem2  7154  1ndom2  7166  ssfiexmid  7178  domfiexmid  7182  exmidpw2en  7219  unfiexmid  7225  unfiin  7233  inresflem  7400  casefun  7425  caserel  7427  caseinj  7429  omp1eomlem  7434  omp1eom  7435  endjusym  7436  djufun  7444  djuinj  7446  ctssdccl  7451  ctssdclemr  7452  nninfex  7461  infnninf  7464  fodjuomnilemdc  7484  ctssexmid  7490  exmidonfinlem  7545  dju1p1e2  7549  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  pw1dom2  7586  onntri35  7596  onntri45  7600  2oneel  7622  2omotaplemst  7624  acnccim  7638  1lt2pi  7707  indpi  7709  1nq  7733  rec1nq  7762  1lt2nq  7773  ltaddnq  7774  halfnqq  7777  prarloclemarch2  7786  prarloclemlt  7860  prarloclemcalc  7869  genpelxp  7878  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  cauappcvgprlemladd  8025  caucvgprlemcl  8043  caucvgprprlemcl  8071  suplocexprlemell  8080  suplocexprlemdisj  8087  suplocexprlemub  8090  0r  8117  1sr  8118  m1r  8119  m1p1sr  8127  m1m1sr  8128  0lt1sr  8132  1ne0sr  8133  1idsr  8135  recexgt0sr  8140  prsradd  8153  caucvgsrlemoffres  8167  caucvgsr  8169  mappsrprg  8171  map2psrprg  8172  pitonnlem1p1  8213  pitonnlem2  8214  pitoregt0  8216  peano2nnnn  8220  axi2m1  8242  axprecex  8247  axcnre  8248  nnindnn  8260  nntopi  8261  0cn  8318  addcli  8330  mulcli  8331  mulcomi  8332  readdcli  8339  remulcli  8340  rexpssxrxp  8370  ltrelxr  8386  gtneii  8422  lttri3i  8424  letri3i  8425  ltnsymi  8426  lenlti  8427  ltlei  8428  mulgt0i  8436  mulgt0ii  8437  0lt1  8454  addcomi  8471  pncan3oi  8543  resubcli  8590  subcli  8603  pncan3i  8604  negsubi  8605  subnegi  8606  subeq0i  8607  neg11i  8608  negcon1i  8609  negcon2i  8610  mulneg1i  8732  mulneg2i  8733  mul2negi  8734  addgt0ii  8820  ltnegi  8822  lenegi  8823  ltnegcon2i  8824  lesub0i  8825  ltaddposi  8826  posdifi  8827  ltnegcon1i  8828  lenegcon1i  8829  subge0i  8830  1ap0  8920  ltapii  8965  recrecapi  9076  dividapi  9077  div0api  9078  rec11apii  9093  divdiv32api  9099  recgt0ii  9239  ltrecii  9250  ltdiv23ii  9259  sup3exmid  9289  nnssre  9310  nnind  9322  nnmulcli  9328  nnsubi  9346  0le2  9396  1lt3  9480  2lt4  9482  1lt4  9483  3lt5  9485  2lt5  9486  1lt5  9487  4lt6  9489  3lt6  9490  2lt6  9491  1lt6  9492  5lt7  9494  4lt7  9495  3lt7  9496  2lt7  9497  1lt7  9498  6lt8  9500  5lt8  9501  4lt8  9502  3lt8  9503  2lt8  9504  1lt8  9505  7lt9  9507  6lt9  9508  5lt9  9509  4lt9  9510  3lt9  9511  2lt9  9512  1lt9  9513  2muline0  9534  nn0addcli  9604  nn0mulcli  9605  nn0addge1i  9615  nn0addge2i  9616  dfz2  9721  halfnz  9746  9p1e10  9783  numnncl  9790  numltc  9811  le9lt10  9812  nummac  9830  8lt10  9917  7lt10  9918  6lt10  9919  5lt10  9920  4lt10  9921  3lt10  9922  2lt10  9923  1lt10  9924  eluzaddi  9958  eluzsubi  9959  uzuzle23  9971  uzuzle24  9972  uzuzle34  9973  eluz2nn  9975  eluz4eluz2  9977  eluzge3nn  9981  divfnzn  10030  elq  10031  qreccl  10051  xrltnr  10191  mnfltpnf  10197  xaddmnf1  10260  pnfaddmnf  10262  mnfaddpnf  10263  xrex  10268  xaddid1  10274  xsubge0  10293  xposdif  10294  xleaddadd  10299  elicc2i  10351  ioomax  10360  iccmax  10361  ioopos  10362  elxrge0  10390  iccshftri  10407  iccshftli  10409  iccdili  10411  icccntri  10413  unitssre  10418  fz10  10460  fz00m1  10461  fzpreddisj  10488  fz0to4untppr  10541  dfrp2  10708  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  frecfzennn  10876  xnn0nnen  10887  fnn0nninf  10888  fxnn0nninf  10889  0tonninf  10890  1tonninf  10891  m1expcl2  11011  m1expcl  11012  nn0expcli  11015  sqmuli  11072  cu2  11088  i3  11091  subsqi  11099  binom2subi  11105  bcpasc  11218  4bc2eq6  11227  hashinfom  11231  prhash2ex  11264  hashp1i  11265  lsw0g  11367  swrdccat3blem  11525  rei  11679  imi  11680  readdi  11708  imaddi  11709  remuli  11710  immuli  11711  cjaddi  11712  cjmuli  11713  ipcni  11714  crrei  11716  crimi  11717  rexfiuz  11769  sqrt1  11826  sqrt4  11827  sqrt9  11828  abs1  11852  sqrtmulii  11915  abslti  11919  abslei  11920  abssubi  11931  absmuli  11932  sqabsaddi  11933  sqabssubi  11934  abstrii  11936  fimaxre2  12008  climz  12074  abscn2  12097  recn2  12099  imcn2  12100  climabs  12102  climre  12104  climim  12105  fsumcnv  12220  fsumrelem  12254  fsumre  12255  fsumim  12256  arisum2  12282  expcnv  12287  geo2sum2  12298  geo2lim  12299  0.999...  12304  geoihalfsum  12305  fprodcnv  12408  fprodge0  12420  fprodge1  12422  ege2le3  12454  ef0  12455  reeff1  12483  tan0  12514  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  sinltxirr  12544  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  sincos1sgn  12548  sincos2sgn  12549  cos12dec  12551  egt2lt3  12563  epos  12564  ene1  12568  eap1  12569  3dvds  12647  3dvdsdec  12648  3dvds2dec  12649  odd2np1lem  12655  n2dvds1  12695  z4even  12699  ndvdsi  12716  flodddiv4  12719  bitsp1o  12736  0bits  12742  gcd0val  12753  6gcd4e2  12788  3lcm2e6woprm  12880  6lcm4e12  12881  3lcm2e6  12955  sqrt2irrlem  12956  phimullem  13023  pockthi  13157  4sqlem19  13208  dec2dvds  13210  dec5dvds2  13212  dec2nprm  13214  modxai  13215  mod2xnegi  13218  gcdi  13220  gcdmodi  13221  numexpp1  13224  karatsuba  13230  2exp7  13234  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilemofi  13268  ballotfilem1  13269  ballotfilem2  13277  ballotfilemfmpn  13283  ballotfilemefi  13286  ballotfilemodife  13289  ballotfilem4  13290  ballotfilemiex  13293  ballotfilemimin  13298  ballotfilemic  13299  ballotfilemsval  13301  ballotfilemsdom  13304  ballotfilemsel1i  13305  ballotfilemsima  13308  ballotfilemrval  13310  ballotfilemfrceq  13321  ballotfilemfrcn0  13322  ballotfilem1ri  13327  ballotfilem7  13328  ballotfilem8  13329  ballotfilemth  13330  xpnnen  13334  xpomen  13335  ennnfonelemj0  13341  ennnfonelem0  13345  ennnfonelemhf1o  13353  exmidunben  13366  qnnen  13371  unct  13382  setscom  13441  strleun  13507  prdsvallem  13670  imasival  13676  ismgm  13726  fn0g  13744  fngzsum  13757  issgrp  13767  ismnddef  13780  isghm  14095  prdsex  14221  isrng  14282  rngmgpf  14285  isring  14353  mgpf  14364  dfrhm2  14510  rhmex  14513  isdomn  14627  rmodislmod  14737  lidlmex  14861  mopnset  14938  cnfldstr  14944  cnfldcj  14951  cnfld0  14957  cnfldplusf  14960  zringcrng  14976  zringmulr  14983  zringmpg  14990  znval  15020  psrval  15099  fnpsr  15100  fnmpl  15133  txtopi  15411  txunii  15414  upxp  15422  uptx  15424  cnmpt1st  15438  cnmpt2nd  15439  txswaphmeolem  15470  qtopbasss  15671  cnmet  15680  cnfldms  15686  cnopncntop  15694  cnopn  15695  remet  15698  blssioo  15703  tgqioo  15705  tgioo2cntop  15707  tgioo2  15709  divcnap  15715  abscncf  15735  recncf  15736  imcncf  15737  cjcncf  15738  mulc1cncf  15739  cncfcn1cntop  15744  idcncf  15751  cdivcncfap  15754  expcncf  15759  cnrehmeocntop  15760  maxcncf  15765  mincncf  15766  ivthreinc  15795  hovercncf  15796  limccnp2lem  15826  limccnp2cntop  15827  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvrecap  15863  dveflem  15876  dvef  15877  sincn  15919  coscn  15920  reeff1oleme  15922  reeff1o  15923  cosz12  15931  sin0pilem1  15932  sin0pilem2  15933  pipos  15939  sinhalfpilem  15942  sincosq1lem  15976  sincosq1sgn  15977  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  cosq14gt0  15983  cosq23lt0  15984  coseq0q4123  15985  coseq00topi  15986  coseq0negpitopi  15987  tangtx  15989  sincos4thpi  15991  tan4thpi  15992  sincos6thpi  15993  pigt3  15995  cosordlem  16000  cosq34lt1  16001  cos02pilt1  16002  cos0pilt1  16003  ioocosf1o  16005  negpitopissre  16006  log1  16017  loge  16018  2logb9irr  16126  sqrt2cxp2logb9e3  16130  2logb9irrap  16132  log2tlbndlog2  16139  log2ublem1  16140  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  birthdaylog2  16147  ppi1  16176  ppi1i  16177  ppi2i  16178  mpodvdsmulf1o  16185  fsumdvdsmul  16186  1sgm2ppw  16190  ppiublem1  16192  ppiublem2  16193  ppiqub  16194  bpos1lem  16207  lgsdir2lem2  16246  lgsdir2lem3  16247  lgseisenlem4  16290  2lgsoddprmlem3  16328  2sqlem9  16341  2sqlem10  16342  opvtxfvi  16366  opiedgfvi  16367  umgrbien  16449  usgrprc  16591  vtxdfifiun  16636  upgr2wlkdc  16716  konigsbergvtx  16821  konigsbergiedg  16822  konigsbergumgr  16826  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  konigsberg  16832  ex-fl  16837  ex-ceil  16838  ex-bc  16841  ex-dvds  16842  ex-gcd  16843  bj-charfunbi  16935  bj-unex  17043  bj-nn0suc0  17074  bj-nntrans  17075  bj-nnelirr  17077  012of  17121  2o01f  17122  pwle2  17126  nnsf  17146  peano3nninf  17148  exmidsbthrlem  17165  sbthom  17169  repiecelem  17172  repiecele0  17173  repiecege0  17174  isomninnlem  17177  iooref1o  17181  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  apdiff  17195  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  dceqnconst  17208  dcapnconst  17209  nconstwlpolemgt0  17212  taupi  17221