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  724  mp3an  1374  barbara  2179  eqeq12i  2246  el2v  2819  vtocl2  2870  spc2ev  2913  sbc2ie  3114  csbieb  3180  sseq12i  3266  uneq12i  3371  ineq12i  3420  ifssun  3637  nelpri  3713  ralpr  3744  rexpr  3745  preq12i  3773  dfop  3882  opeq12i  3888  breq12i  4118  mpteq2ia  4196  exmidundif  4319  exmidundifim  4320  opex  4345  opi2  4349  opth2  4356  opeqsn  4369  opeqpr  4370  uniop  4372  opelopaba  4384  braba  4385  opelopab  4390  brab  4391  opelopabaf  4392  unex  4562  snnex  4569  op1stb  4599  ifelpwun  4604  ifex  4607  onun2i  4613  onsucssi  4628  ontriexmidim  4644  ontr2exmid  4647  onsucsssucexmid  4649  onsucelsucexmid  4652  opthreg  4678  tfis  4705  finds  4722  finds2  4723  nnregexmid  4743  xpeq12i  4771  opelvv  4800  eqrelriiv  4844  eqrelrdv  4846  xpss  4858  xpex  4866  relop  4905  brco  4926  opelcnv  4937  brcnv  4938  asymref  5148  codir  5151  ssrnres  5205  dmprop  5237  dfco2  5262  cossxp  5285  cocnvss  5288  coex  5308  funsn  5404  fnsn  5410  feq23i  5503  resasplitss  5544  fabex  5555  fvex  5690  xpsn  5854  fmptap  5874  opabex  5910  acexmidlemv  6048  oveq12i  6062  oprabid  6082  oprabss  6139  caovcom  6212  opabex3  6315  iunex  6316  oprabex  6321  ofmres  6329  op1st  6340  op2nd  6341  fo1st  6351  fo2nd  6352  mpoex  6410  1stconst  6417  2ndconst  6418  algrflem  6425  dftpos4  6494  tpostpos  6495  tpossym  6507  frecex  6625  frecfnom  6632  2oex  6664  sucinc  6678  fnoei  6685  oeiexg  6686  nnacli  6715  nnmcli  6716  elec  6808  ecovcom  6876  ecovass  6878  ecovdi  6880  fnmap  6889  mapval  6894  elmap  6911  elpm  6913  elpm2  6914  map0  6924  ixpconst  6943  entri  7026  endisj  7075  xpcomco  7077  phplem2  7107  1ndom2  7119  ssfiexmid  7131  domfiexmid  7135  exmidpw2en  7172  unfiexmid  7178  unfiin  7186  inresflem  7351  casefun  7376  caserel  7378  caseinj  7380  omp1eomlem  7385  omp1eom  7386  endjusym  7387  djufun  7395  djuinj  7397  ctssdccl  7402  ctssdclemr  7403  nninfex  7412  infnninf  7415  fodjuomnilemdc  7435  ctssexmid  7441  exmidonfinlem  7496  dju1p1e2  7500  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  pw1dom2  7537  onntri35  7547  onntri45  7551  2oneel  7570  2omotaplemst  7572  acnccim  7586  1lt2pi  7655  indpi  7657  1nq  7681  rec1nq  7710  1lt2nq  7721  ltaddnq  7722  halfnqq  7725  prarloclemarch2  7734  prarloclemlt  7808  prarloclemcalc  7817  genpelxp  7826  ltexprlempr  7923  recexprlempr  7947  cauappcvgprlemcl  7968  cauappcvgprlemladd  7973  caucvgprlemcl  7991  caucvgprprlemcl  8019  suplocexprlemell  8028  suplocexprlemdisj  8035  suplocexprlemub  8038  0r  8065  1sr  8066  m1r  8067  m1p1sr  8075  m1m1sr  8076  0lt1sr  8080  1ne0sr  8081  1idsr  8083  recexgt0sr  8088  prsradd  8101  caucvgsrlemoffres  8115  caucvgsr  8117  mappsrprg  8119  map2psrprg  8120  pitonnlem1p1  8161  pitonnlem2  8162  pitoregt0  8164  peano2nnnn  8168  axi2m1  8190  axprecex  8195  axcnre  8196  nnindnn  8208  nntopi  8209  0cn  8266  addcli  8278  mulcli  8279  mulcomi  8280  readdcli  8287  remulcli  8288  rexpssxrxp  8318  ltrelxr  8334  gtneii  8369  lttri3i  8371  letri3i  8372  ltnsymi  8373  lenlti  8374  ltlei  8375  mulgt0i  8383  mulgt0ii  8384  0lt1  8400  addcomi  8417  pncan3oi  8489  resubcli  8536  subcli  8549  pncan3i  8550  negsubi  8551  subnegi  8552  subeq0i  8553  neg11i  8554  negcon1i  8555  negcon2i  8556  mulneg1i  8677  mulneg2i  8678  mul2negi  8679  addgt0ii  8765  ltnegi  8767  lenegi  8768  ltnegcon2i  8769  lesub0i  8770  ltaddposi  8771  posdifi  8772  ltnegcon1i  8773  lenegcon1i  8774  subge0i  8775  1ap0  8864  ltapii  8909  recrecapi  9018  dividapi  9019  div0api  9020  rec11apii  9035  divdiv32api  9041  recgt0ii  9181  ltrecii  9192  ltdiv23ii  9201  sup3exmid  9231  nnssre  9241  nnind  9253  nnmulcli  9259  nnsubi  9277  0le2  9327  1lt3  9409  2lt4  9411  1lt4  9412  3lt5  9414  2lt5  9415  1lt5  9416  4lt6  9418  3lt6  9419  2lt6  9420  1lt6  9421  5lt7  9423  4lt7  9424  3lt7  9425  2lt7  9426  1lt7  9427  6lt8  9429  5lt8  9430  4lt8  9431  3lt8  9432  2lt8  9433  1lt8  9434  7lt9  9436  6lt9  9437  5lt9  9438  4lt9  9439  3lt9  9440  2lt9  9441  1lt9  9442  2muline0  9463  nn0addcli  9533  nn0mulcli  9534  nn0addge1i  9544  nn0addge2i  9545  dfz2  9650  halfnz  9674  9p1e10  9711  numnncl  9718  numltc  9734  le9lt10  9735  nummac  9753  8lt10  9840  7lt10  9841  6lt10  9842  5lt10  9843  4lt10  9844  3lt10  9845  2lt10  9846  1lt10  9847  eluzaddi  9881  eluzsubi  9882  uzuzle23  9894  uzuzle24  9895  uzuzle34  9896  eluz2nn  9898  eluz4eluz2  9900  eluzge3nn  9904  divfnzn  9953  elq  9954  qreccl  9974  xrltnr  10112  mnfltpnf  10118  xaddmnf1  10181  pnfaddmnf  10183  mnfaddpnf  10184  xrex  10189  xaddid1  10195  xsubge0  10214  xposdif  10215  xleaddadd  10220  elicc2i  10272  ioomax  10281  iccmax  10282  ioopos  10283  elxrge0  10311  iccshftri  10328  iccshftli  10330  iccdili  10332  icccntri  10334  unitssre  10339  fz10  10380  fzpreddisj  10405  fz0to4untppr  10458  dfrp2  10623  fldiv4p1lem1div2  10665  fldiv4lem1div2  10667  frecfzennn  10788  xnn0nnen  10799  fnn0nninf  10800  fxnn0nninf  10801  0tonninf  10802  1tonninf  10803  m1expcl2  10923  m1expcl  10924  nn0expcli  10927  sqmuli  10984  cu2  11000  i3  11003  subsqi  11011  binom2subi  11017  bcpasc  11128  4bc2eq6  11137  hashinfom  11141  prhash2ex  11174  hashp1i  11175  lsw0g  11273  swrdccat3blem  11431  rei  11584  imi  11585  readdi  11613  imaddi  11614  remuli  11615  immuli  11616  cjaddi  11617  cjmuli  11618  ipcni  11619  crrei  11621  crimi  11622  rexfiuz  11674  sqrt1  11731  sqrt4  11732  sqrt9  11733  abs1  11757  sqrtmulii  11819  abslti  11823  abslei  11824  abssubi  11835  absmuli  11836  sqabsaddi  11837  sqabssubi  11838  abstrii  11840  fimaxre2  11912  climz  11977  abscn2  12000  recn2  12002  imcn2  12003  climabs  12005  climre  12007  climim  12008  fsumcnv  12123  fsumrelem  12157  fsumre  12158  fsumim  12159  arisum2  12185  expcnv  12190  geo2sum2  12201  geo2lim  12202  0.999...  12207  geoihalfsum  12208  fprodcnv  12311  fprodge0  12323  fprodge1  12325  ege2le3  12357  ef0  12358  reeff1  12386  tan0  12417  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos1bnd  12445  cos2bnd  12446  sinltxirr  12447  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  sincos1sgn  12451  sincos2sgn  12452  cos12dec  12454  egt2lt3  12466  epos  12467  ene1  12471  eap1  12472  3dvds  12550  3dvdsdec  12551  3dvds2dec  12552  odd2np1lem  12558  n2dvds1  12598  z4even  12602  ndvdsi  12619  flodddiv4  12622  bitsp1o  12639  0bits  12645  gcd0val  12656  6gcd4e2  12691  3lcm2e6woprm  12783  6lcm4e12  12784  3lcm2e6  12857  sqrt2irrlem  12858  phimullem  12922  pockthi  13056  4sqlem19  13107  dec2dvds  13109  dec5dvds2  13111  dec2nprm  13113  modxai  13114  gcdi  13118  gcdmodi  13119  numexpp1  13122  karatsuba  13128  2exp7  13132  ballotfilemofi  13138  ballotfilem1  13139  ballotfilem2  13142  xpnnen  13145  xpomen  13146  ennnfonelemj0  13152  ennnfonelem0  13156  ennnfonelemhf1o  13164  exmidunben  13177  qnnen  13182  unct  13193  setscom  13252  strleun  13317  prdsex  13482  prdsvallem  13485  imasival  13519  ismgm  13570  fn0g  13588  fngsum  13601  issgrp  13616  ismnddef  13631  isghm  13960  isrng  14078  rngmgpf  14081  isring  14144  mgpf  14155  dfrhm2  14299  rhmex  14302  isdomn  14415  rmodislmod  14499  lidlmex  14623  mopnset  14700  cnfldstr  14706  cnfldcj  14713  cnfld0  14719  cnfldplusf  14722  zringcrng  14740  zringmulr  14747  zringmpg  14754  znval  14784  psrval  14814  fnpsr  14815  fnmpl  14848  txtopi  15126  txunii  15129  upxp  15137  uptx  15139  cnmpt1st  15153  cnmpt2nd  15154  txswaphmeolem  15185  qtopbasss  15386  cnmet  15395  cnfldms  15401  cnopncntop  15409  cnopn  15410  remet  15413  blssioo  15418  tgqioo  15420  tgioo2cntop  15422  tgioo2  15424  divcnap  15430  abscncf  15450  recncf  15451  imcncf  15452  cjcncf  15453  mulc1cncf  15454  cncfcn1cntop  15459  idcncf  15466  cdivcncfap  15469  expcncf  15474  cnrehmeocntop  15475  maxcncf  15480  mincncf  15481  ivthreinc  15510  hovercncf  15511  limccnp2lem  15541  limccnp2cntop  15542  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvrecap  15578  dveflem  15591  dvef  15592  sincn  15634  coscn  15635  reeff1oleme  15637  reeff1o  15638  cosz12  15645  sin0pilem1  15646  sin0pilem2  15647  pipos  15653  sinhalfpilem  15656  sincosq1lem  15690  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  cosq14gt0  15697  cosq23lt0  15698  coseq0q4123  15699  coseq00topi  15700  coseq0negpitopi  15701  tangtx  15703  sincos4thpi  15705  tan4thpi  15706  sincos6thpi  15707  pigt3  15709  cosordlem  15714  cosq34lt1  15715  cos02pilt1  15716  cos0pilt1  15717  ioocosf1o  15719  negpitopissre  15720  log1  15731  loge  15732  2logb9irr  15836  sqrt2cxp2logb9e3  15840  2logb9irrap  15842  mpodvdsmulf1o  15858  fsumdvdsmul  15859  1sgm2ppw  15863  lgsdir2lem2  15902  lgsdir2lem3  15903  lgseisenlem4  15946  2lgsoddprmlem3  15984  2sqlem9  15997  2sqlem10  15998  opvtxfvi  16022  opiedgfvi  16023  umgrbien  16105  usgrprc  16247  vtxdfifiun  16292  upgr2wlkdc  16372  konigsbergvtx  16477  konigsbergiedg  16478  konigsbergumgr  16482  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  konigsberg  16488  ex-fl  16493  ex-ceil  16494  ex-bc  16497  ex-dvds  16498  ex-gcd  16499  bj-charfunbi  16581  bj-unex  16689  bj-nn0suc0  16720  bj-nntrans  16721  bj-nnelirr  16723  012of  16767  2o01f  16768  pwle2  16772  nnsf  16783  peano3nninf  16785  exmidsbthrlem  16802  sbthom  16806  repiecelem  16809  repiecele0  16810  repiecege0  16811  isomninnlem  16814  iooref1o  16818  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  apdiff  16832  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837  dceqnconst  16846  dcapnconst  16847  nconstwlpolemgt0  16850  taupi  16859