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  3856  opeq12i  3862  breq12i  4092  mpteq2ia  4170  exmidundif  4290  exmidundifim  4291  opex  4315  opi2  4319  opth2  4326  opeqsn  4339  opeqpr  4340  uniop  4342  opelopaba  4354  braba  4355  opelopab  4360  brab  4361  opelopabaf  4362  unex  4532  snnex  4539  op1stb  4569  ifelpwun  4574  ifex  4577  onun2i  4583  onsucssi  4598  ontriexmidim  4614  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  opthreg  4648  tfis  4675  finds  4692  finds2  4693  nnregexmid  4713  xpeq12i  4741  opelvv  4769  eqrelriiv  4813  eqrelrdv  4815  xpss  4827  xpex  4834  relop  4872  brco  4893  opelcnv  4904  brcnv  4905  asymref  5114  codir  5117  ssrnres  5171  dmprop  5203  dfco2  5228  cossxp  5251  cocnvss  5254  coex  5274  funsn  5369  fnsn  5375  feq23i  5468  resasplitss  5507  fabex  5516  fvex  5649  xpsn  5813  fmptap  5833  opabex  5867  acexmidlemv  6005  oveq12i  6019  oprabid  6039  oprabss  6096  caovcom  6169  opabex3  6273  iunex  6274  oprabex  6279  ofmres  6287  op1st  6298  op2nd  6299  fo1st  6309  fo2nd  6310  mpoex  6366  1stconst  6373  2ndconst  6374  algrflem  6381  dftpos4  6415  tpostpos  6416  tpossym  6428  frecex  6546  frecfnom  6553  2oex  6585  sucinc  6599  fnoei  6606  oeiexg  6607  nnacli  6636  nnmcli  6637  elec  6729  ecovcom  6797  ecovass  6799  ecovdi  6801  fnmap  6810  mapval  6815  elmap  6832  elpm  6834  elpm2  6835  map0  6844  ixpconst  6863  entri  6946  endisj  6991  xpcomco  6993  phplem2  7022  1ndom2  7034  ssfiexmid  7046  domfiexmid  7048  exmidpw2en  7085  unfiexmid  7091  unfiin  7099  inresflem  7238  casefun  7263  caserel  7265  caseinj  7267  omp1eomlem  7272  omp1eom  7273  endjusym  7274  djufun  7282  djuinj  7284  ctssdccl  7289  ctssdclemr  7290  nninfex  7299  infnninf  7302  fodjuomnilemdc  7322  ctssexmid  7328  exmidonfinlem  7382  dju1p1e2  7386  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  pw1dom2  7423  onntri35  7433  onntri45  7437  2oneel  7453  2omotaplemst  7455  acnccim  7469  1lt2pi  7538  indpi  7540  1nq  7564  rec1nq  7593  1lt2nq  7604  ltaddnq  7605  halfnqq  7608  prarloclemarch2  7617  prarloclemlt  7691  prarloclemcalc  7700  genpelxp  7709  ltexprlempr  7806  recexprlempr  7830  cauappcvgprlemcl  7851  cauappcvgprlemladd  7856  caucvgprlemcl  7874  caucvgprprlemcl  7902  suplocexprlemell  7911  suplocexprlemdisj  7918  suplocexprlemub  7921  0r  7948  1sr  7949  m1r  7950  m1p1sr  7958  m1m1sr  7959  0lt1sr  7963  1ne0sr  7964  1idsr  7966  recexgt0sr  7971  prsradd  7984  caucvgsrlemoffres  7998  caucvgsr  8000  mappsrprg  8002  map2psrprg  8003  pitonnlem1p1  8044  pitonnlem2  8045  pitoregt0  8047  peano2nnnn  8051  axi2m1  8073  axprecex  8078  axcnre  8079  nnindnn  8091  nntopi  8092  0cn  8149  addcli  8161  mulcli  8162  mulcomi  8163  readdcli  8170  remulcli  8171  rexpssxrxp  8202  ltrelxr  8218  gtneii  8253  lttri3i  8255  letri3i  8256  ltnsymi  8257  lenlti  8258  ltlei  8259  mulgt0i  8267  mulgt0ii  8268  0lt1  8284  addcomi  8301  pncan3oi  8373  resubcli  8420  subcli  8433  pncan3i  8434  negsubi  8435  subnegi  8436  subeq0i  8437  neg11i  8438  negcon1i  8439  negcon2i  8440  mulneg1i  8561  mulneg2i  8562  mul2negi  8563  addgt0ii  8649  ltnegi  8651  lenegi  8652  ltnegcon2i  8653  lesub0i  8654  ltaddposi  8655  posdifi  8656  ltnegcon1i  8657  lenegcon1i  8658  subge0i  8659  1ap0  8748  ltapii  8793  recrecapi  8902  dividapi  8903  div0api  8904  rec11apii  8919  divdiv32api  8925  recgt0ii  9065  ltrecii  9076  ltdiv23ii  9085  sup3exmid  9115  nnssre  9125  nnind  9137  nnmulcli  9143  nnsubi  9161  0le2  9211  1lt3  9293  2lt4  9295  1lt4  9296  3lt5  9298  2lt5  9299  1lt5  9300  4lt6  9302  3lt6  9303  2lt6  9304  1lt6  9305  5lt7  9307  4lt7  9308  3lt7  9309  2lt7  9310  1lt7  9311  6lt8  9313  5lt8  9314  4lt8  9315  3lt8  9316  2lt8  9317  1lt8  9318  7lt9  9320  6lt9  9321  5lt9  9322  4lt9  9323  3lt9  9324  2lt9  9325  1lt9  9326  2muline0  9347  nn0addcli  9417  nn0mulcli  9418  nn0addge1i  9428  nn0addge2i  9429  dfz2  9530  halfnz  9554  9p1e10  9591  numnncl  9598  numltc  9614  le9lt10  9615  nummac  9633  8lt10  9720  7lt10  9721  6lt10  9722  5lt10  9723  4lt10  9724  3lt10  9725  2lt10  9726  1lt10  9727  eluzaddi  9761  eluzsubi  9762  eluz2nn  9773  eluz4eluz2  9774  uzuzle23  9778  eluzge3nn  9779  divfnzn  9828  elq  9829  qreccl  9849  xrltnr  9987  mnfltpnf  9993  xaddmnf1  10056  pnfaddmnf  10058  mnfaddpnf  10059  xrex  10064  xaddid1  10070  xsubge0  10089  xposdif  10090  xleaddadd  10095  elicc2i  10147  ioomax  10156  iccmax  10157  ioopos  10158  elxrge0  10186  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  unitssre  10213  fz10  10254  fzpreddisj  10279  fz0to4untppr  10332  dfrp2  10495  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  frecfzennn  10660  xnn0nnen  10671  fnn0nninf  10672  fxnn0nninf  10673  0tonninf  10674  1tonninf  10675  m1expcl2  10795  m1expcl  10796  nn0expcli  10799  sqmuli  10856  cu2  10872  i3  10875  subsqi  10883  binom2subi  10889  bcpasc  11000  4bc2eq6  11008  hashinfom  11012  prhash2ex  11044  hashp1i  11045  lsw0g  11133  swrdccat3blem  11286  rei  11425  imi  11426  readdi  11454  imaddi  11455  remuli  11456  immuli  11457  cjaddi  11458  cjmuli  11459  ipcni  11460  crrei  11462  crimi  11463  rexfiuz  11515  sqrt1  11572  sqrt4  11573  sqrt9  11574  abs1  11598  sqrtmulii  11660  abslti  11664  abslei  11665  abssubi  11676  absmuli  11677  sqabsaddi  11678  sqabssubi  11679  abstrii  11681  fimaxre2  11753  climz  11818  abscn2  11841  recn2  11843  imcn2  11844  climabs  11846  climre  11848  climim  11849  fsumcnv  11963  fsumrelem  11997  fsumre  11998  fsumim  11999  arisum2  12025  expcnv  12030  geo2sum2  12041  geo2lim  12042  0.999...  12047  geoihalfsum  12048  fprodcnv  12151  fprodge0  12163  fprodge1  12165  ege2le3  12197  ef0  12198  reeff1  12226  tan0  12257  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  cos1bnd  12285  cos2bnd  12286  sinltxirr  12287  sin01gt0  12288  cos01gt0  12289  sin02gt0  12290  sincos1sgn  12291  sincos2sgn  12292  cos12dec  12294  egt2lt3  12306  epos  12307  ene1  12311  eap1  12312  3dvds  12390  3dvdsdec  12391  3dvds2dec  12392  odd2np1lem  12398  n2dvds1  12438  z4even  12442  ndvdsi  12459  flodddiv4  12462  bitsp1o  12479  0bits  12485  gcd0val  12496  6gcd4e2  12531  3lcm2e6woprm  12623  6lcm4e12  12624  3lcm2e6  12697  sqrt2irrlem  12698  phimullem  12762  pockthi  12896  4sqlem19  12947  dec2dvds  12949  dec5dvds2  12951  dec2nprm  12953  modxai  12954  gcdi  12958  gcdmodi  12959  numexpp1  12962  karatsuba  12968  2exp7  12972  xpnnen  12980  xpomen  12981  ennnfonelemj0  12987  ennnfonelem0  12991  ennnfonelemhf1o  12999  exmidunben  13012  qnnen  13017  unct  13028  setscom  13087  strleun  13152  prdsex  13317  prdsvallem  13320  imasival  13354  ismgm  13405  fn0g  13423  fngsum  13436  issgrp  13451  ismnddef  13466  isghm  13795  isrng  13912  rngmgpf  13915  isring  13978  mgpf  13989  dfrhm2  14133  rhmex  14136  isdomn  14248  rmodislmod  14330  lidlmex  14454  mopnset  14531  cnfldstr  14537  cnfldcj  14544  cnfld0  14550  cnfldplusf  14553  zringcrng  14571  zringmulr  14578  zringmpg  14585  znval  14615  psrval  14645  fnpsr  14646  fnmpl  14672  txtopi  14950  txunii  14953  upxp  14961  uptx  14963  cnmpt1st  14977  cnmpt2nd  14978  txswaphmeolem  15009  qtopbasss  15210  cnmet  15219  cnfldms  15225  cnopncntop  15233  cnopn  15234  remet  15237  blssioo  15242  tgqioo  15244  tgioo2cntop  15246  tgioo2  15248  divcnap  15254  abscncf  15274  recncf  15275  imcncf  15276  cjcncf  15277  mulc1cncf  15278  cncfcn1cntop  15283  idcncf  15290  cdivcncfap  15293  expcncf  15298  cnrehmeocntop  15299  maxcncf  15304  mincncf  15305  ivthreinc  15334  hovercncf  15335  limccnp2lem  15365  limccnp2cntop  15366  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvrecap  15402  dveflem  15415  dvef  15416  sincn  15458  coscn  15459  reeff1oleme  15461  reeff1o  15462  cosz12  15469  sin0pilem1  15470  sin0pilem2  15471  pipos  15477  sinhalfpilem  15480  sincosq1lem  15514  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  sinq12gt0  15519  cosq14gt0  15521  cosq23lt0  15522  coseq0q4123  15523  coseq00topi  15524  coseq0negpitopi  15525  tangtx  15527  sincos4thpi  15529  tan4thpi  15530  sincos6thpi  15531  pigt3  15533  cosordlem  15538  cosq34lt1  15539  cos02pilt1  15540  cos0pilt1  15541  ioocosf1o  15543  negpitopissre  15544  log1  15555  loge  15556  2logb9irr  15660  sqrt2cxp2logb9e3  15664  2logb9irrap  15666  mpodvdsmulf1o  15679  fsumdvdsmul  15680  1sgm2ppw  15684  lgsdir2lem2  15723  lgsdir2lem3  15724  lgseisenlem4  15767  2lgsoddprmlem3  15805  2sqlem9  15818  2sqlem10  15819  opvtxfvi  15843  opiedgfvi  15844  umgrbien  15925  vtxdfifiun  16056  upgr2wlkdc  16116  ex-fl  16144  ex-ceil  16145  ex-bc  16148  ex-dvds  16149  ex-gcd  16150  bj-charfunbi  16229  bj-unex  16337  bj-nn0suc0  16368  bj-nntrans  16369  bj-nnelirr  16371  012of  16416  2o01f  16417  pwle2  16423  nnsf  16431  peano3nninf  16433  exmidsbthrlem  16450  sbthom  16454  isomninnlem  16458  iooref1o  16462  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  apdiff  16476  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480  dceqnconst  16488  dcapnconst  16489  nconstwlpolemgt0  16492  taupi  16501