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  2805  vtocl2  2856  spc2ev  2899  sbc2ie  3100  csbieb  3166  sseq12i  3252  uneq12i  3356  ineq12i  3403  ifssun  3617  nelpri  3690  ralpr  3721  rexpr  3722  preq12i  3748  dfop  3855  opeq12i  3861  breq12i  4091  mpteq2ia  4169  exmidundif  4289  exmidundifim  4290  opex  4314  opi2  4318  opth2  4325  opeqsn  4338  opeqpr  4339  uniop  4341  opelopaba  4353  braba  4354  opelopab  4359  brab  4360  opelopabaf  4361  unex  4531  snnex  4538  op1stb  4568  ifelpwun  4573  ifex  4576  onun2i  4582  onsucssi  4597  ontriexmidim  4613  ontr2exmid  4616  onsucsssucexmid  4618  onsucelsucexmid  4621  opthreg  4647  tfis  4674  finds  4691  finds2  4692  nnregexmid  4712  xpeq12i  4740  opelvv  4768  eqrelriiv  4812  eqrelrdv  4814  xpss  4826  xpex  4833  relop  4871  brco  4892  opelcnv  4903  brcnv  4904  asymref  5113  codir  5116  ssrnres  5170  dmprop  5202  dfco2  5227  cossxp  5250  cocnvss  5253  coex  5273  funsn  5368  fnsn  5374  feq23i  5467  resasplitss  5504  fabex  5513  fvex  5646  xpsn  5810  fmptap  5828  opabex  5862  acexmidlemv  5998  oveq12i  6012  oprabid  6032  oprabss  6089  caovcom  6162  opabex3  6265  iunex  6266  oprabex  6271  ofmres  6279  op1st  6290  op2nd  6291  fo1st  6301  fo2nd  6302  mpoex  6358  1stconst  6365  2ndconst  6366  algrflem  6373  dftpos4  6407  tpostpos  6408  tpossym  6420  frecex  6538  frecfnom  6545  sucinc  6589  fnoei  6596  oeiexg  6597  nnacli  6626  nnmcli  6627  elec  6719  ecovcom  6787  ecovass  6789  ecovdi  6791  fnmap  6800  mapval  6805  elmap  6822  elpm  6824  elpm2  6825  map0  6834  ixpconst  6853  entri  6936  endisj  6979  xpcomco  6981  phplem2  7010  1ndom2  7022  ssfiexmid  7034  domfiexmid  7036  exmidpw2en  7070  unfiexmid  7076  unfiin  7084  inresflem  7223  casefun  7248  caserel  7250  caseinj  7252  omp1eomlem  7257  omp1eom  7258  endjusym  7259  djufun  7267  djuinj  7269  ctssdccl  7274  ctssdclemr  7275  nninfex  7284  infnninf  7287  fodjuomnilemdc  7307  ctssexmid  7313  exmidonfinlem  7367  dju1p1e2  7371  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidaclem  7386  pw1dom2  7408  onntri35  7418  onntri45  7422  2oneel  7438  2omotaplemst  7440  acnccim  7454  1lt2pi  7523  indpi  7525  1nq  7549  rec1nq  7578  1lt2nq  7589  ltaddnq  7590  halfnqq  7593  prarloclemarch2  7602  prarloclemlt  7676  prarloclemcalc  7685  genpelxp  7694  ltexprlempr  7791  recexprlempr  7815  cauappcvgprlemcl  7836  cauappcvgprlemladd  7841  caucvgprlemcl  7859  caucvgprprlemcl  7887  suplocexprlemell  7896  suplocexprlemdisj  7903  suplocexprlemub  7906  0r  7933  1sr  7934  m1r  7935  m1p1sr  7943  m1m1sr  7944  0lt1sr  7948  1ne0sr  7949  1idsr  7951  recexgt0sr  7956  prsradd  7969  caucvgsrlemoffres  7983  caucvgsr  7985  mappsrprg  7987  map2psrprg  7988  pitonnlem1p1  8029  pitonnlem2  8030  pitoregt0  8032  peano2nnnn  8036  axi2m1  8058  axprecex  8063  axcnre  8064  nnindnn  8076  nntopi  8077  0cn  8134  addcli  8146  mulcli  8147  mulcomi  8148  readdcli  8155  remulcli  8156  rexpssxrxp  8187  ltrelxr  8203  gtneii  8238  lttri3i  8240  letri3i  8241  ltnsymi  8242  lenlti  8243  ltlei  8244  mulgt0i  8252  mulgt0ii  8253  0lt1  8269  addcomi  8286  pncan3oi  8358  resubcli  8405  subcli  8418  pncan3i  8419  negsubi  8420  subnegi  8421  subeq0i  8422  neg11i  8423  negcon1i  8424  negcon2i  8425  mulneg1i  8546  mulneg2i  8547  mul2negi  8548  addgt0ii  8634  ltnegi  8636  lenegi  8637  ltnegcon2i  8638  lesub0i  8639  ltaddposi  8640  posdifi  8641  ltnegcon1i  8642  lenegcon1i  8643  subge0i  8644  1ap0  8733  ltapii  8778  recrecapi  8887  dividapi  8888  div0api  8889  rec11apii  8904  divdiv32api  8910  recgt0ii  9050  ltrecii  9061  ltdiv23ii  9070  sup3exmid  9100  nnssre  9110  nnind  9122  nnmulcli  9128  nnsubi  9146  0le2  9196  1lt3  9278  2lt4  9280  1lt4  9281  3lt5  9283  2lt5  9284  1lt5  9285  4lt6  9287  3lt6  9288  2lt6  9289  1lt6  9290  5lt7  9292  4lt7  9293  3lt7  9294  2lt7  9295  1lt7  9296  6lt8  9298  5lt8  9299  4lt8  9300  3lt8  9301  2lt8  9302  1lt8  9303  7lt9  9305  6lt9  9306  5lt9  9307  4lt9  9308  3lt9  9309  2lt9  9310  1lt9  9311  2muline0  9332  nn0addcli  9402  nn0mulcli  9403  nn0addge1i  9413  nn0addge2i  9414  dfz2  9515  halfnz  9539  9p1e10  9576  numnncl  9583  numltc  9599  le9lt10  9600  nummac  9618  8lt10  9705  7lt10  9706  6lt10  9707  5lt10  9708  4lt10  9709  3lt10  9710  2lt10  9711  1lt10  9712  eluzaddi  9745  eluzsubi  9746  eluz2nn  9757  eluz4eluz2  9758  uzuzle23  9762  eluzge3nn  9763  divfnzn  9812  elq  9813  qreccl  9833  xrltnr  9971  mnfltpnf  9977  xaddmnf1  10040  pnfaddmnf  10042  mnfaddpnf  10043  xrex  10048  xaddid1  10054  xsubge0  10073  xposdif  10074  xleaddadd  10079  elicc2i  10131  ioomax  10140  iccmax  10141  ioopos  10142  elxrge0  10170  iccshftri  10187  iccshftli  10189  iccdili  10191  icccntri  10193  unitssre  10197  fz10  10238  fzpreddisj  10263  fz0to4untppr  10316  dfrp2  10478  fldiv4p1lem1div2  10520  fldiv4lem1div2  10522  frecfzennn  10643  xnn0nnen  10654  fnn0nninf  10655  fxnn0nninf  10656  0tonninf  10657  1tonninf  10658  m1expcl2  10778  m1expcl  10779  nn0expcli  10782  sqmuli  10839  cu2  10855  i3  10858  subsqi  10866  binom2subi  10872  bcpasc  10983  4bc2eq6  10991  hashinfom  10995  prhash2ex  11026  hashp1i  11027  lsw0g  11115  swrdccat3blem  11266  rei  11405  imi  11406  readdi  11434  imaddi  11435  remuli  11436  immuli  11437  cjaddi  11438  cjmuli  11439  ipcni  11440  crrei  11442  crimi  11443  rexfiuz  11495  sqrt1  11552  sqrt4  11553  sqrt9  11554  abs1  11578  sqrtmulii  11640  abslti  11644  abslei  11645  abssubi  11656  absmuli  11657  sqabsaddi  11658  sqabssubi  11659  abstrii  11661  fimaxre2  11733  climz  11798  abscn2  11821  recn2  11823  imcn2  11824  climabs  11826  climre  11828  climim  11829  fsumcnv  11943  fsumrelem  11977  fsumre  11978  fsumim  11979  arisum2  12005  expcnv  12010  geo2sum2  12021  geo2lim  12022  0.999...  12027  geoihalfsum  12028  fprodcnv  12131  fprodge0  12143  fprodge1  12145  ege2le3  12177  ef0  12178  reeff1  12206  tan0  12237  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  cos1bnd  12265  cos2bnd  12266  sinltxirr  12267  sin01gt0  12268  cos01gt0  12269  sin02gt0  12270  sincos1sgn  12271  sincos2sgn  12272  cos12dec  12274  egt2lt3  12286  epos  12287  ene1  12291  eap1  12292  3dvds  12370  3dvdsdec  12371  3dvds2dec  12372  odd2np1lem  12378  n2dvds1  12418  z4even  12422  ndvdsi  12439  flodddiv4  12442  bitsp1o  12459  0bits  12465  gcd0val  12476  6gcd4e2  12511  3lcm2e6woprm  12603  6lcm4e12  12604  3lcm2e6  12677  sqrt2irrlem  12678  phimullem  12742  pockthi  12876  4sqlem19  12927  dec2dvds  12929  dec5dvds2  12931  dec2nprm  12933  modxai  12934  gcdi  12938  gcdmodi  12939  numexpp1  12942  karatsuba  12948  2exp7  12952  xpnnen  12960  xpomen  12961  ennnfonelemj0  12967  ennnfonelem0  12971  ennnfonelemhf1o  12979  exmidunben  12992  qnnen  12997  unct  13008  setscom  13067  strleun  13132  prdsex  13297  prdsvallem  13300  imasival  13334  ismgm  13385  fn0g  13403  fngsum  13416  issgrp  13431  ismnddef  13446  isghm  13775  isrng  13892  rngmgpf  13895  isring  13958  mgpf  13969  dfrhm2  14112  rhmex  14115  isdomn  14227  rmodislmod  14309  lidlmex  14433  mopnset  14510  cnfldstr  14516  cnfldcj  14523  cnfld0  14529  cnfldplusf  14532  zringcrng  14550  zringmulr  14557  zringmpg  14564  znval  14594  psrval  14624  fnpsr  14625  fnmpl  14651  txtopi  14929  txunii  14932  upxp  14940  uptx  14942  cnmpt1st  14956  cnmpt2nd  14957  txswaphmeolem  14988  qtopbasss  15189  cnmet  15198  cnfldms  15204  cnopncntop  15212  cnopn  15213  remet  15216  blssioo  15221  tgqioo  15223  tgioo2cntop  15225  tgioo2  15227  divcnap  15233  abscncf  15253  recncf  15254  imcncf  15255  cjcncf  15256  mulc1cncf  15257  cncfcn1cntop  15262  idcncf  15269  cdivcncfap  15272  expcncf  15277  cnrehmeocntop  15278  maxcncf  15283  mincncf  15284  ivthreinc  15313  hovercncf  15314  limccnp2lem  15344  limccnp2cntop  15345  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvrecap  15381  dveflem  15394  dvef  15395  sincn  15437  coscn  15438  reeff1oleme  15440  reeff1o  15441  cosz12  15448  sin0pilem1  15449  sin0pilem2  15450  pipos  15456  sinhalfpilem  15459  sincosq1lem  15493  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  cosq14gt0  15500  cosq23lt0  15501  coseq0q4123  15502  coseq00topi  15503  coseq0negpitopi  15504  tangtx  15506  sincos4thpi  15508  tan4thpi  15509  sincos6thpi  15510  pigt3  15512  cosordlem  15517  cosq34lt1  15518  cos02pilt1  15519  cos0pilt1  15520  ioocosf1o  15522  negpitopissre  15523  log1  15534  loge  15535  2logb9irr  15639  sqrt2cxp2logb9e3  15643  2logb9irrap  15645  mpodvdsmulf1o  15658  fsumdvdsmul  15659  1sgm2ppw  15663  lgsdir2lem2  15702  lgsdir2lem3  15703  lgseisenlem4  15746  2lgsoddprmlem3  15784  2sqlem9  15797  2sqlem10  15798  opvtxfvi  15822  opiedgfvi  15823  umgrbien  15904  ex-fl  16047  ex-ceil  16048  ex-bc  16051  ex-dvds  16052  ex-gcd  16053  bj-charfunbi  16132  bj-unex  16240  bj-nn0suc0  16271  bj-nntrans  16272  bj-nnelirr  16274  012of  16316  2o01f  16317  pwle2  16323  nnsf  16330  peano3nninf  16332  exmidsbthrlem  16349  sbthom  16353  isomninnlem  16357  iooref1o  16361  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  apdiff  16375  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379  dceqnconst  16387  dcapnconst  16388  nconstwlpolemgt0  16391  taupi  16400