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  717  mp3an  1349  barbara  2151  eqeq12i  2218  vtocl2  2827  spc2ev  2868  sbc2ie  3069  csbieb  3134  sseq12i  3220  uneq12i  3324  ineq12i  3371  ifssun  3584  nelpri  3656  ralpr  3687  rexpr  3688  preq12i  3714  dfop  3817  opeq12i  3823  breq12i  4052  mpteq2ia  4129  exmidundif  4249  exmidundifim  4250  opex  4272  opi2  4276  opth2  4283  opeqsn  4295  opeqpr  4296  uniop  4298  opelopaba  4310  braba  4311  opelopab  4316  brab  4317  opelopabaf  4318  unex  4486  snnex  4493  op1stb  4523  ifelpwun  4528  ifex  4531  onun2i  4537  onsucssi  4552  ontriexmidim  4568  ontr2exmid  4571  onsucsssucexmid  4573  onsucelsucexmid  4576  opthreg  4602  tfis  4629  finds  4646  finds2  4647  nnregexmid  4667  xpeq12i  4695  opelvv  4723  eqrelriiv  4767  eqrelrdv  4769  xpss  4781  xpex  4788  relop  4826  brco  4847  opelcnv  4858  brcnv  4859  asymref  5065  codir  5068  ssrnres  5122  dmprop  5154  dfco2  5179  cossxp  5202  cocnvss  5205  coex  5225  funsn  5316  fnsn  5322  feq23i  5414  resasplitss  5449  fabex  5458  fvex  5590  xpsn  5750  fmptap  5764  opabex  5798  acexmidlemv  5932  oveq12i  5946  oprabid  5966  oprabss  6021  caovcom  6094  opabex3  6197  iunex  6198  oprabex  6203  ofmres  6211  op1st  6222  op2nd  6223  fo1st  6233  fo2nd  6234  mpoex  6290  1stconst  6297  2ndconst  6298  algrflem  6305  dftpos4  6339  tpostpos  6340  tpossym  6352  frecex  6470  frecfnom  6477  sucinc  6521  fnoei  6528  oeiexg  6529  nnacli  6558  nnmcli  6559  elec  6651  ecovcom  6719  ecovass  6721  ecovdi  6723  fnmap  6732  mapval  6737  elmap  6754  elpm  6756  elpm2  6757  map0  6766  ixpconst  6785  entri  6863  endisj  6901  xpcomco  6903  phplem2  6932  ssfiexmid  6955  domfiexmid  6957  exmidpw2en  6991  unfiexmid  6997  unfiin  7005  inresflem  7144  casefun  7169  caserel  7171  caseinj  7173  omp1eomlem  7178  omp1eom  7179  endjusym  7180  djufun  7188  djuinj  7190  ctssdccl  7195  ctssdclemr  7196  nninfex  7205  infnninf  7208  fodjuomnilemdc  7228  ctssexmid  7234  exmidonfinlem  7283  dju1p1e2  7287  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  exmidaclem  7302  pw1dom2  7321  onntri35  7331  onntri45  7335  2oneel  7350  2omotaplemst  7352  acnccim  7366  1lt2pi  7435  indpi  7437  1nq  7461  rec1nq  7490  1lt2nq  7501  ltaddnq  7502  halfnqq  7505  prarloclemarch2  7514  prarloclemlt  7588  prarloclemcalc  7597  genpelxp  7606  ltexprlempr  7703  recexprlempr  7727  cauappcvgprlemcl  7748  cauappcvgprlemladd  7753  caucvgprlemcl  7771  caucvgprprlemcl  7799  suplocexprlemell  7808  suplocexprlemdisj  7815  suplocexprlemub  7818  0r  7845  1sr  7846  m1r  7847  m1p1sr  7855  m1m1sr  7856  0lt1sr  7860  1ne0sr  7861  1idsr  7863  recexgt0sr  7868  prsradd  7881  caucvgsrlemoffres  7895  caucvgsr  7897  mappsrprg  7899  map2psrprg  7900  pitonnlem1p1  7941  pitonnlem2  7942  pitoregt0  7944  peano2nnnn  7948  axi2m1  7970  axprecex  7975  axcnre  7976  nnindnn  7988  nntopi  7989  0cn  8046  addcli  8058  mulcli  8059  mulcomi  8060  readdcli  8067  remulcli  8068  rexpssxrxp  8099  ltrelxr  8115  gtneii  8150  lttri3i  8152  letri3i  8153  ltnsymi  8154  lenlti  8155  ltlei  8156  mulgt0i  8164  mulgt0ii  8165  0lt1  8181  addcomi  8198  pncan3oi  8270  resubcli  8317  subcli  8330  pncan3i  8331  negsubi  8332  subnegi  8333  subeq0i  8334  neg11i  8335  negcon1i  8336  negcon2i  8337  mulneg1i  8458  mulneg2i  8459  mul2negi  8460  addgt0ii  8546  ltnegi  8548  lenegi  8549  ltnegcon2i  8550  lesub0i  8551  ltaddposi  8552  posdifi  8553  ltnegcon1i  8554  lenegcon1i  8555  subge0i  8556  1ap0  8645  ltapii  8690  recrecapi  8799  dividapi  8800  div0api  8801  rec11apii  8816  divdiv32api  8822  recgt0ii  8962  ltrecii  8973  ltdiv23ii  8982  sup3exmid  9012  nnssre  9022  nnind  9034  nnmulcli  9040  nnsubi  9058  0le2  9108  1lt3  9190  2lt4  9192  1lt4  9193  3lt5  9195  2lt5  9196  1lt5  9197  4lt6  9199  3lt6  9200  2lt6  9201  1lt6  9202  5lt7  9204  4lt7  9205  3lt7  9206  2lt7  9207  1lt7  9208  6lt8  9210  5lt8  9211  4lt8  9212  3lt8  9213  2lt8  9214  1lt8  9215  7lt9  9217  6lt9  9218  5lt9  9219  4lt9  9220  3lt9  9221  2lt9  9222  1lt9  9223  2muline0  9244  nn0addcli  9314  nn0mulcli  9315  nn0addge1i  9325  nn0addge2i  9326  dfz2  9427  halfnz  9451  9p1e10  9488  numnncl  9495  numltc  9511  le9lt10  9512  nummac  9530  8lt10  9617  7lt10  9618  6lt10  9619  5lt10  9620  4lt10  9621  3lt10  9622  2lt10  9623  1lt10  9624  eluzaddi  9657  eluzsubi  9658  eluz2nn  9669  eluz4eluz2  9670  uzuzle23  9674  eluzge3nn  9675  divfnzn  9724  elq  9725  qreccl  9745  xrltnr  9883  mnfltpnf  9889  xaddmnf1  9952  pnfaddmnf  9954  mnfaddpnf  9955  xrex  9960  xaddid1  9966  xsubge0  9985  xposdif  9986  xleaddadd  9991  elicc2i  10043  ioomax  10052  iccmax  10053  ioopos  10054  elxrge0  10082  iccshftri  10099  iccshftli  10101  iccdili  10103  icccntri  10105  unitssre  10109  fz10  10150  fzpreddisj  10175  fz0to4untppr  10228  dfrp2  10387  fldiv4p1lem1div2  10429  fldiv4lem1div2  10431  frecfzennn  10552  xnn0nnen  10563  fnn0nninf  10564  fxnn0nninf  10565  0tonninf  10566  1tonninf  10567  m1expcl2  10687  m1expcl  10688  nn0expcli  10691  sqmuli  10748  cu2  10764  i3  10767  subsqi  10775  binom2subi  10781  bcpasc  10892  4bc2eq6  10900  hashinfom  10904  prhash2ex  10935  hashp1i  10936  lsw0g  11017  rei  11129  imi  11130  readdi  11158  imaddi  11159  remuli  11160  immuli  11161  cjaddi  11162  cjmuli  11163  ipcni  11164  crrei  11166  crimi  11167  rexfiuz  11219  sqrt1  11276  sqrt4  11277  sqrt9  11278  abs1  11302  sqrtmulii  11364  abslti  11368  abslei  11369  abssubi  11380  absmuli  11381  sqabsaddi  11382  sqabssubi  11383  abstrii  11385  fimaxre2  11457  climz  11522  abscn2  11545  recn2  11547  imcn2  11548  climabs  11550  climre  11552  climim  11553  fsumcnv  11667  fsumrelem  11701  fsumre  11702  fsumim  11703  arisum2  11729  expcnv  11734  geo2sum2  11745  geo2lim  11746  0.999...  11751  geoihalfsum  11752  fprodcnv  11855  fprodge0  11867  fprodge1  11869  ege2le3  11901  ef0  11902  reeff1  11930  tan0  11961  ef01bndlem  11986  sin01bnd  11987  cos01bnd  11988  cos1bnd  11989  cos2bnd  11990  sinltxirr  11991  sin01gt0  11992  cos01gt0  11993  sin02gt0  11994  sincos1sgn  11995  sincos2sgn  11996  cos12dec  11998  egt2lt3  12010  epos  12011  ene1  12015  eap1  12016  3dvds  12094  3dvdsdec  12095  3dvds2dec  12096  odd2np1lem  12102  n2dvds1  12142  z4even  12146  ndvdsi  12163  flodddiv4  12166  bitsp1o  12183  0bits  12189  gcd0val  12200  6gcd4e2  12235  3lcm2e6woprm  12327  6lcm4e12  12328  3lcm2e6  12401  sqrt2irrlem  12402  phimullem  12466  pockthi  12600  4sqlem19  12651  dec2dvds  12653  dec5dvds2  12655  dec2nprm  12657  modxai  12658  gcdi  12662  gcdmodi  12663  numexpp1  12666  karatsuba  12672  2exp7  12676  xpnnen  12684  xpomen  12685  ennnfonelemj0  12691  ennnfonelem0  12695  ennnfonelemhf1o  12703  exmidunben  12716  qnnen  12721  unct  12732  setscom  12791  strleun  12855  prdsex  13019  prdsvallem  13022  imasival  13056  ismgm  13107  fn0g  13125  fngsum  13138  issgrp  13153  ismnddef  13168  isghm  13497  isrng  13614  rngmgpf  13617  isring  13680  mgpf  13691  dfrhm2  13834  rhmex  13837  isdomn  13949  rmodislmod  14031  lidlmex  14155  mopnset  14232  cnfldstr  14238  cnfldcj  14245  cnfld0  14251  cnfldplusf  14254  zringcrng  14272  zringmulr  14279  zringmpg  14286  znval  14316  psrval  14346  fnpsr  14347  fnmpl  14373  txtopi  14651  txunii  14654  upxp  14662  uptx  14664  cnmpt1st  14678  cnmpt2nd  14679  txswaphmeolem  14710  qtopbasss  14911  cnmet  14920  cnfldms  14926  cnopncntop  14934  cnopn  14935  remet  14938  blssioo  14943  tgqioo  14945  tgioo2cntop  14947  tgioo2  14949  divcnap  14955  abscncf  14975  recncf  14976  imcncf  14977  cjcncf  14978  mulc1cncf  14979  cncfcn1cntop  14984  idcncf  14991  cdivcncfap  14994  expcncf  14999  cnrehmeocntop  15000  maxcncf  15005  mincncf  15006  ivthreinc  15035  hovercncf  15036  limccnp2lem  15066  limccnp2cntop  15067  dvcnp2cntop  15089  dvaddxxbr  15091  dvmulxxbr  15092  dvcoapbr  15097  dvrecap  15103  dveflem  15116  dvef  15117  sincn  15159  coscn  15160  reeff1oleme  15162  reeff1o  15163  cosz12  15170  sin0pilem1  15171  sin0pilem2  15172  pipos  15178  sinhalfpilem  15181  sincosq1lem  15215  sincosq1sgn  15216  sincosq2sgn  15217  sincosq3sgn  15218  sincosq4sgn  15219  sinq12gt0  15220  cosq14gt0  15222  cosq23lt0  15223  coseq0q4123  15224  coseq00topi  15225  coseq0negpitopi  15226  tangtx  15228  sincos4thpi  15230  tan4thpi  15231  sincos6thpi  15232  pigt3  15234  cosordlem  15239  cosq34lt1  15240  cos02pilt1  15241  cos0pilt1  15242  ioocosf1o  15244  negpitopissre  15245  log1  15256  loge  15257  2logb9irr  15361  sqrt2cxp2logb9e3  15365  2logb9irrap  15367  mpodvdsmulf1o  15380  fsumdvdsmul  15381  1sgm2ppw  15385  lgsdir2lem2  15424  lgsdir2lem3  15425  lgseisenlem4  15468  2lgsoddprmlem3  15506  2sqlem9  15519  2sqlem10  15520  ex-fl  15525  ex-ceil  15526  ex-bc  15529  ex-dvds  15530  ex-gcd  15531  bj-charfunbi  15611  bj-unex  15719  bj-nn0suc0  15750  bj-nntrans  15751  bj-nnelirr  15753  012of  15794  2o01f  15795  pwle2  15799  nnsf  15806  peano3nninf  15808  exmidsbthrlem  15825  sbthom  15829  isomninnlem  15833  iooref1o  15837  trilpolemisumle  15841  trilpolemeq1  15843  trilpolemlt1  15844  apdiff  15851  iswomninnlem  15852  iswomni0  15854  ismkvnnlem  15855  dceqnconst  15863  dcapnconst  15864  nconstwlpolemgt0  15867  taupi  15876