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  7401  casefun  7426  caserel  7428  caseinj  7430  omp1eomlem  7435  omp1eom  7436  endjusym  7437  djufun  7445  djuinj  7447  ctssdccl  7452  ctssdclemr  7453  nninfex  7462  infnninf  7465  fodjuomnilemdc  7485  ctssexmid  7491  exmidonfinlem  7546  dju1p1e2  7550  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  pw1dom2  7587  onntri35  7597  onntri45  7601  2oneel  7623  2omotaplemst  7625  acnccim  7639  1lt2pi  7708  indpi  7710  1nq  7734  rec1nq  7763  1lt2nq  7774  ltaddnq  7775  halfnqq  7778  prarloclemarch2  7787  prarloclemlt  7861  prarloclemcalc  7870  genpelxp  7879  ltexprlempr  7976  recexprlempr  8000  cauappcvgprlemcl  8021  cauappcvgprlemladd  8026  caucvgprlemcl  8044  caucvgprprlemcl  8072  suplocexprlemell  8081  suplocexprlemdisj  8088  suplocexprlemub  8091  0r  8118  1sr  8119  m1r  8120  m1p1sr  8128  m1m1sr  8129  0lt1sr  8133  1ne0sr  8134  1idsr  8136  recexgt0sr  8141  prsradd  8154  caucvgsrlemoffres  8168  caucvgsr  8170  mappsrprg  8172  map2psrprg  8173  pitonnlem1p1  8214  pitonnlem2  8215  pitoregt0  8217  peano2nnnn  8221  axi2m1  8243  axprecex  8248  axcnre  8249  nnindnn  8261  nntopi  8262  0cn  8319  addcli  8331  mulcli  8332  mulcomi  8333  readdcli  8340  remulcli  8341  rexpssxrxp  8371  ltrelxr  8387  gtneii  8423  lttri3i  8425  letri3i  8426  ltnsymi  8427  lenlti  8428  ltlei  8429  mulgt0i  8437  mulgt0ii  8438  0lt1  8455  addcomi  8472  pncan3oi  8544  resubcli  8591  subcli  8604  pncan3i  8605  negsubi  8606  subnegi  8607  subeq0i  8608  neg11i  8609  negcon1i  8610  negcon2i  8611  mulneg1i  8733  mulneg2i  8734  mul2negi  8735  addgt0ii  8821  ltnegi  8823  lenegi  8824  ltnegcon2i  8825  lesub0i  8826  ltaddposi  8827  posdifi  8828  ltnegcon1i  8829  lenegcon1i  8830  subge0i  8831  1ap0  8921  ltapii  8966  recrecapi  9077  dividapi  9078  div0api  9079  rec11apii  9094  divdiv32api  9100  recgt0ii  9240  ltrecii  9251  ltdiv23ii  9260  sup3exmid  9290  nnssre  9311  nnind  9323  nnmulcli  9329  nnsubi  9347  0le2  9397  1lt3  9481  2lt4  9483  1lt4  9484  3lt5  9486  2lt5  9487  1lt5  9488  4lt6  9490  3lt6  9491  2lt6  9492  1lt6  9493  5lt7  9495  4lt7  9496  3lt7  9497  2lt7  9498  1lt7  9499  6lt8  9501  5lt8  9502  4lt8  9503  3lt8  9504  2lt8  9505  1lt8  9506  7lt9  9508  6lt9  9509  5lt9  9510  4lt9  9511  3lt9  9512  2lt9  9513  1lt9  9514  2muline0  9535  nn0addcli  9605  nn0mulcli  9606  nn0addge1i  9616  nn0addge2i  9617  dfz2  9722  halfnz  9747  9p1e10  9784  numnncl  9791  numltc  9812  le9lt10  9813  nummac  9831  8lt10  9918  7lt10  9919  6lt10  9920  5lt10  9921  4lt10  9922  3lt10  9923  2lt10  9924  1lt10  9925  eluzaddi  9959  eluzsubi  9960  uzuzle23  9972  uzuzle24  9973  uzuzle34  9974  eluz2nn  9976  eluz4eluz2  9978  eluzge3nn  9982  divfnzn  10031  elq  10032  qreccl  10052  xrltnr  10192  mnfltpnf  10198  xaddmnf1  10261  pnfaddmnf  10263  mnfaddpnf  10264  xrex  10269  xaddid1  10275  xsubge0  10294  xposdif  10295  xleaddadd  10300  elicc2i  10352  ioomax  10361  iccmax  10362  ioopos  10363  elxrge0  10391  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  unitssre  10419  fz10  10461  fz00m1  10462  fzpreddisj  10489  fz0to4untppr  10542  dfrp2  10709  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  frecfzennn  10878  xnn0nnen  10889  fnn0nninf  10890  fxnn0nninf  10891  0tonninf  10892  1tonninf  10893  m1expcl2  11013  m1expcl  11014  nn0expcli  11017  sqmuli  11074  cu2  11090  i3  11093  subsqi  11101  binom2subi  11107  bcpasc  11220  4bc2eq6  11229  hashinfom  11233  prhash2ex  11266  hashp1i  11267  lsw0g  11369  swrdccat3blem  11527  rei  11681  imi  11682  readdi  11710  imaddi  11711  remuli  11712  immuli  11713  cjaddi  11714  cjmuli  11715  ipcni  11716  crrei  11718  crimi  11719  rexfiuz  11771  sqrt1  11828  sqrt4  11829  sqrt9  11830  abs1  11854  sqrtmulii  11917  abslti  11921  abslei  11922  abssubi  11933  absmuli  11934  sqabsaddi  11935  sqabssubi  11936  abstrii  11938  fimaxre2  12010  fiidxsupcl  12012  climz  12077  abscn2  12100  recn2  12102  imcn2  12103  climabs  12105  climre  12107  climim  12108  fsumcnv  12223  fsumrelem  12257  fsumre  12258  fsumim  12259  arisum2  12285  expcnv  12290  geo2sum2  12301  geo2lim  12302  0.999...  12307  geoihalfsum  12308  fprodcnv  12411  fprodge0  12423  fprodge1  12425  ege2le3  12457  ef0  12458  reeff1  12486  tan0  12517  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  sinltxirr  12547  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  sincos1sgn  12551  sincos2sgn  12552  cos12dec  12554  egt2lt3  12566  epos  12567  ene1  12571  eap1  12572  3dvds  12650  3dvdsdec  12651  3dvds2dec  12652  odd2np1lem  12658  n2dvds1  12698  z4even  12702  ndvdsi  12719  flodddiv4  12722  bitsp1o  12739  0bits  12745  gcd0val  12756  6gcd4e2  12791  3lcm2e6woprm  12883  6lcm4e12  12884  3lcm2e6  12958  sqrt2irrlem  12959  phimullem  13026  pockthi  13160  4sqlem19  13211  dec2dvds  13213  dec5dvds2  13215  dec2nprm  13217  modxai  13218  mod2xnegi  13221  gcdi  13223  gcdmodi  13224  numexpp1  13227  karatsuba  13233  2exp7  13237  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilemofi  13271  ballotfilem1  13272  ballotfilem2  13280  ballotfilemfmpn  13286  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilem4  13293  ballotfilemiex  13296  ballotfilemimin  13301  ballotfilemic  13302  ballotfilemsval  13304  ballotfilemsdom  13307  ballotfilemsel1i  13308  ballotfilemsima  13311  ballotfilemrval  13313  ballotfilemfrceq  13324  ballotfilemfrcn0  13325  ballotfilem1ri  13330  ballotfilem7  13331  ballotfilem8  13332  ballotfilemth  13333  xpnnen  13337  xpomen  13338  ennnfonelemj0  13344  ennnfonelem0  13348  ennnfonelemhf1o  13356  exmidunben  13369  qnnen  13374  unct  13385  setscom  13444  strleun  13511  prdsvallem  13674  imasival  13680  ismgm  13730  fn0g  13748  fngzsum  13761  issgrp  13771  ismnddef  13784  isghm  14099  prdsex  14256  isrng  14317  rngmgpf  14320  isring  14388  mgpf  14399  dfrhm2  14545  rhmex  14548  isdomn  14662  rmodislmod  14772  lidlmex  14896  mopnset  14973  cnfldstr  14979  cnfldcj  14986  cnfld0  14992  cnfldplusf  14995  zringcrng  15011  zringmulr  15018  zringmpg  15025  znval  15055  psrval  15134  fnpsr  15135  fnmpl  15175  txtopi  15453  txunii  15456  upxp  15464  uptx  15466  cnmpt1st  15480  cnmpt2nd  15481  txswaphmeolem  15512  qtopbasss  15713  cnmet  15722  cnfldms  15728  cnopncntop  15736  cnopn  15737  remet  15740  blssioo  15745  tgqioo  15747  tgioo2cntop  15749  tgioo2  15751  divcnap  15757  abscncf  15777  recncf  15778  imcncf  15779  cjcncf  15780  mulc1cncf  15781  cncfcn1cntop  15786  idcncf  15793  cdivcncfap  15796  expcncf  15801  cnrehmeocntop  15802  maxcncf  15807  mincncf  15808  ivthreinc  15837  hovercncf  15838  limccnp2lem  15868  limccnp2cntop  15869  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvrecap  15905  dveflem  15918  dvef  15919  sincn  15961  coscn  15962  reeff1oleme  15964  reeff1o  15965  cosz12  15973  sin0pilem1  15974  sin0pilem2  15975  pipos  15981  sinhalfpilem  15984  sincosq1lem  16018  sincosq1sgn  16019  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  cosq14gt0  16025  cosq23lt0  16026  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  sincos4thpi  16033  tan4thpi  16034  sincos6thpi  16035  pigt3  16037  cosordlem  16042  cosq34lt1  16043  cos02pilt1  16044  cos0pilt1  16045  ioocosf1o  16047  negpitopissre  16048  log1  16059  loge  16060  2logb9irr  16168  sqrt2cxp2logb9e3  16172  2logb9irrap  16174  log2tlbndlog2  16181  log2ublem1  16182  log2ublem2  16183  log2ublem3  16184  log2ublog2  16185  birthdaylog2  16189  ppi1  16231  cht1  16232  ppi1i  16233  ppi2i  16234  cht2  16237  cht3  16238  chtqrpcl  16240  mpodvdsmulf1o  16245  fsumdvdsmul  16246  1sgm2ppw  16250  ppiublem1  16252  ppiublem2  16253  ppiqub  16254  chtqub  16257  bpos1lem  16270  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsdir2lem2  16314  lgsdir2lem3  16315  lgseisenlem4  16358  2lgsoddprmlem3  16396  2sqlem9  16409  2sqlem10  16410  opvtxfvi  16434  opiedgfvi  16435  umgrbien  16517  usgrprc  16659  vtxdfifiun  16704  upgr2wlkdc  16784  konigsbergvtx  16889  konigsbergiedg  16890  konigsbergumgr  16894  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem5  16899  konigsberg  16900  ex-fl  16905  ex-ceil  16906  ex-bc  16909  ex-dvds  16910  ex-gcd  16911  bj-charfunbi  17003  bj-unex  17111  bj-nn0suc0  17142  bj-nntrans  17143  bj-nnelirr  17145  012of  17189  2o01f  17190  pwle2  17194  nnsf  17214  peano3nninf  17216  exmidsbthrlem  17233  sbthom  17237  repiecelem  17240  repiecele0  17241  repiecege0  17242  isomninnlem  17245  iooref1o  17249  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  apdiff  17264  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  dceqnconst  17277  dcapnconst  17278  nconstwlpolemgt0  17281  taupi  17290