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  8421  lttri3i  8423  letri3i  8424  ltnsymi  8425  lenlti  8426  ltlei  8427  mulgt0i  8435  mulgt0ii  8436  0lt1  8453  addcomi  8470  pncan3oi  8542  resubcli  8589  subcli  8602  pncan3i  8603  negsubi  8604  subnegi  8605  subeq0i  8606  neg11i  8607  negcon1i  8608  negcon2i  8609  mulneg1i  8731  mulneg2i  8732  mul2negi  8733  addgt0ii  8819  ltnegi  8821  lenegi  8822  ltnegcon2i  8823  lesub0i  8824  ltaddposi  8825  posdifi  8826  ltnegcon1i  8827  lenegcon1i  8828  subge0i  8829  1ap0  8918  ltapii  8963  recrecapi  9074  dividapi  9075  div0api  9076  rec11apii  9091  divdiv32api  9097  recgt0ii  9237  ltrecii  9248  ltdiv23ii  9257  sup3exmid  9287  nnssre  9308  nnind  9320  nnmulcli  9326  nnsubi  9344  0le2  9394  1lt3  9476  2lt4  9478  1lt4  9479  3lt5  9481  2lt5  9482  1lt5  9483  4lt6  9485  3lt6  9486  2lt6  9487  1lt6  9488  5lt7  9490  4lt7  9491  3lt7  9492  2lt7  9493  1lt7  9494  6lt8  9496  5lt8  9497  4lt8  9498  3lt8  9499  2lt8  9500  1lt8  9501  7lt9  9503  6lt9  9504  5lt9  9505  4lt9  9506  3lt9  9507  2lt9  9508  1lt9  9509  2muline0  9530  nn0addcli  9600  nn0mulcli  9601  nn0addge1i  9611  nn0addge2i  9612  dfz2  9717  halfnz  9742  9p1e10  9779  numnncl  9786  numltc  9802  le9lt10  9803  nummac  9821  8lt10  9908  7lt10  9909  6lt10  9910  5lt10  9911  4lt10  9912  3lt10  9913  2lt10  9914  1lt10  9915  eluzaddi  9949  eluzsubi  9950  uzuzle23  9962  uzuzle24  9963  uzuzle34  9964  eluz2nn  9966  eluz4eluz2  9968  eluzge3nn  9972  divfnzn  10021  elq  10022  qreccl  10042  xrltnr  10181  mnfltpnf  10187  xaddmnf1  10250  pnfaddmnf  10252  mnfaddpnf  10253  xrex  10258  xaddid1  10264  xsubge0  10283  xposdif  10284  xleaddadd  10289  elicc2i  10341  ioomax  10350  iccmax  10351  ioopos  10352  elxrge0  10380  iccshftri  10397  iccshftli  10399  iccdili  10401  icccntri  10403  unitssre  10408  fz10  10450  fz00m1  10451  fzpreddisj  10478  fz0to4untppr  10531  dfrp2  10698  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  frecfzennn  10863  xnn0nnen  10874  fnn0nninf  10875  fxnn0nninf  10876  0tonninf  10877  1tonninf  10878  m1expcl2  10998  m1expcl  10999  nn0expcli  11002  sqmuli  11059  cu2  11075  i3  11078  subsqi  11086  binom2subi  11092  bcpasc  11204  4bc2eq6  11213  hashinfom  11217  prhash2ex  11250  hashp1i  11251  lsw0g  11353  swrdccat3blem  11511  rei  11665  imi  11666  readdi  11694  imaddi  11695  remuli  11696  immuli  11697  cjaddi  11698  cjmuli  11699  ipcni  11700  crrei  11702  crimi  11703  rexfiuz  11755  sqrt1  11812  sqrt4  11813  sqrt9  11814  abs1  11838  sqrtmulii  11900  abslti  11904  abslei  11905  abssubi  11916  absmuli  11917  sqabsaddi  11918  sqabssubi  11919  abstrii  11921  fimaxre2  11993  climz  12058  abscn2  12081  recn2  12083  imcn2  12084  climabs  12086  climre  12088  climim  12089  fsumcnv  12204  fsumrelem  12238  fsumre  12239  fsumim  12240  arisum2  12266  expcnv  12271  geo2sum2  12282  geo2lim  12283  0.999...  12288  geoihalfsum  12289  fprodcnv  12392  fprodge0  12404  fprodge1  12406  ege2le3  12438  ef0  12439  reeff1  12467  tan0  12498  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  sinltxirr  12528  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  sincos1sgn  12532  sincos2sgn  12533  cos12dec  12535  egt2lt3  12547  epos  12548  ene1  12552  eap1  12553  3dvds  12631  3dvdsdec  12632  3dvds2dec  12633  odd2np1lem  12639  n2dvds1  12679  z4even  12683  ndvdsi  12700  flodddiv4  12703  bitsp1o  12720  0bits  12726  gcd0val  12737  6gcd4e2  12772  3lcm2e6woprm  12864  6lcm4e12  12865  3lcm2e6  12938  sqrt2irrlem  12939  phimullem  13003  pockthi  13137  4sqlem19  13188  dec2dvds  13190  dec5dvds2  13192  dec2nprm  13194  modxai  13195  gcdi  13199  gcdmodi  13200  numexpp1  13203  karatsuba  13209  2exp7  13213  ballotfilemofi  13219  ballotfilem1  13220  ballotfilem2  13228  ballotfilemfmpn  13234  ballotfilemefi  13237  ballotfilemodife  13240  ballotfilem4  13241  ballotfilemiex  13244  ballotfilemimin  13249  ballotfilemic  13250  ballotfilemsval  13252  ballotfilemsdom  13255  ballotfilemsel1i  13256  ballotfilemsima  13259  ballotfilemrval  13261  ballotfilemfrceq  13272  ballotfilemfrcn0  13273  ballotfilem1ri  13278  ballotfilem7  13279  ballotfilem8  13280  ballotfilemth  13281  xpnnen  13285  xpomen  13286  ennnfonelemj0  13292  ennnfonelem0  13296  ennnfonelemhf1o  13304  exmidunben  13317  qnnen  13322  unct  13333  setscom  13392  strleun  13458  prdsvallem  13621  imasival  13627  ismgm  13677  fn0g  13695  fngzsum  13708  issgrp  13718  ismnddef  13731  isghm  14046  prdsex  14172  isrng  14233  rngmgpf  14236  isring  14304  mgpf  14315  dfrhm2  14461  rhmex  14464  isdomn  14578  rmodislmod  14688  lidlmex  14812  mopnset  14889  cnfldstr  14895  cnfldcj  14902  cnfld0  14908  cnfldplusf  14911  zringcrng  14927  zringmulr  14934  zringmpg  14941  znval  14971  psrval  15050  fnpsr  15051  fnmpl  15084  txtopi  15362  txunii  15365  upxp  15373  uptx  15375  cnmpt1st  15389  cnmpt2nd  15390  txswaphmeolem  15421  qtopbasss  15622  cnmet  15631  cnfldms  15637  cnopncntop  15645  cnopn  15646  remet  15649  blssioo  15654  tgqioo  15656  tgioo2cntop  15658  tgioo2  15660  divcnap  15666  abscncf  15686  recncf  15687  imcncf  15688  cjcncf  15689  mulc1cncf  15690  cncfcn1cntop  15695  idcncf  15702  cdivcncfap  15705  expcncf  15710  cnrehmeocntop  15711  maxcncf  15716  mincncf  15717  ivthreinc  15746  hovercncf  15747  limccnp2lem  15777  limccnp2cntop  15778  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvrecap  15814  dveflem  15827  dvef  15828  sincn  15870  coscn  15871  reeff1oleme  15873  reeff1o  15874  cosz12  15881  sin0pilem1  15882  sin0pilem2  15883  pipos  15889  sinhalfpilem  15892  sincosq1lem  15926  sincosq1sgn  15927  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  cosq14gt0  15933  cosq23lt0  15934  coseq0q4123  15935  coseq00topi  15936  coseq0negpitopi  15937  tangtx  15939  sincos4thpi  15941  tan4thpi  15942  sincos6thpi  15943  pigt3  15945  cosordlem  15950  cosq34lt1  15951  cos02pilt1  15952  cos0pilt1  15953  ioocosf1o  15955  negpitopissre  15956  log1  15967  loge  15968  2logb9irr  16073  sqrt2cxp2logb9e3  16077  2logb9irrap  16079  log2tlbndlog2  16082  log2ublem1  16083  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  birthdaylog2  16090  mpodvdsmulf1o  16104  fsumdvdsmul  16105  1sgm2ppw  16109  lgsdir2lem2  16148  lgsdir2lem3  16149  lgseisenlem4  16192  2lgsoddprmlem3  16230  2sqlem9  16243  2sqlem10  16244  opvtxfvi  16268  opiedgfvi  16269  umgrbien  16351  usgrprc  16493  vtxdfifiun  16538  upgr2wlkdc  16618  konigsbergvtx  16723  konigsbergiedg  16724  konigsbergumgr  16728  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  konigsberg  16734  ex-fl  16739  ex-ceil  16740  ex-bc  16743  ex-dvds  16744  ex-gcd  16745  bj-charfunbi  16837  bj-unex  16945  bj-nn0suc0  16976  bj-nntrans  16977  bj-nnelirr  16979  012of  17023  2o01f  17024  pwle2  17028  nnsf  17048  peano3nninf  17050  exmidsbthrlem  17067  sbthom  17071  repiecelem  17074  repiecele0  17075  repiecege0  17076  isomninnlem  17079  iooref1o  17083  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  apdiff  17097  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  dceqnconst  17110  dcapnconst  17111  nconstwlpolemgt0  17114  taupi  17123