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  723  mp3an  1373  barbara  2178  eqeq12i  2245  el2v  2808  vtocl2  2859  spc2ev  2902  sbc2ie  3103  csbieb  3169  sseq12i  3255  uneq12i  3359  ineq12i  3406  ifssun  3620  nelpri  3693  ralpr  3724  rexpr  3725  preq12i  3753  dfop  3861  opeq12i  3867  breq12i  4097  mpteq2ia  4175  exmidundif  4296  exmidundifim  4297  opex  4321  opi2  4325  opth2  4332  opeqsn  4345  opeqpr  4346  uniop  4348  opelopaba  4360  braba  4361  opelopab  4366  brab  4367  opelopabaf  4368  unex  4538  snnex  4545  op1stb  4575  ifelpwun  4580  ifex  4583  onun2i  4589  onsucssi  4604  ontriexmidim  4620  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  opthreg  4654  tfis  4681  finds  4698  finds2  4699  nnregexmid  4719  xpeq12i  4747  opelvv  4776  eqrelriiv  4820  eqrelrdv  4822  xpss  4834  xpex  4842  relop  4880  brco  4901  opelcnv  4912  brcnv  4913  asymref  5122  codir  5125  ssrnres  5179  dmprop  5211  dfco2  5236  cossxp  5259  cocnvss  5262  coex  5282  funsn  5378  fnsn  5384  feq23i  5477  resasplitss  5516  fabex  5525  fvex  5659  xpsn  5824  fmptap  5844  opabex  5878  acexmidlemv  6016  oveq12i  6030  oprabid  6050  oprabss  6107  caovcom  6180  opabex3  6284  iunex  6285  oprabex  6290  ofmres  6298  op1st  6309  op2nd  6310  fo1st  6320  fo2nd  6321  mpoex  6379  1stconst  6386  2ndconst  6387  algrflem  6394  dftpos4  6429  tpostpos  6430  tpossym  6442  frecex  6560  frecfnom  6567  2oex  6599  sucinc  6613  fnoei  6620  oeiexg  6621  nnacli  6650  nnmcli  6651  elec  6743  ecovcom  6811  ecovass  6813  ecovdi  6815  fnmap  6824  mapval  6829  elmap  6846  elpm  6848  elpm2  6849  map0  6858  ixpconst  6877  entri  6960  endisj  7008  xpcomco  7010  phplem2  7039  1ndom2  7051  ssfiexmid  7063  domfiexmid  7067  exmidpw2en  7104  unfiexmid  7110  unfiin  7118  inresflem  7259  casefun  7284  caserel  7286  caseinj  7288  omp1eomlem  7293  omp1eom  7294  endjusym  7295  djufun  7303  djuinj  7305  ctssdccl  7310  ctssdclemr  7311  nninfex  7320  infnninf  7323  fodjuomnilemdc  7343  ctssexmid  7349  exmidonfinlem  7404  dju1p1e2  7408  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  pw1dom2  7445  onntri35  7455  onntri45  7459  2oneel  7475  2omotaplemst  7477  acnccim  7491  1lt2pi  7560  indpi  7562  1nq  7586  rec1nq  7615  1lt2nq  7626  ltaddnq  7627  halfnqq  7630  prarloclemarch2  7639  prarloclemlt  7713  prarloclemcalc  7722  genpelxp  7731  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  cauappcvgprlemladd  7878  caucvgprlemcl  7896  caucvgprprlemcl  7924  suplocexprlemell  7933  suplocexprlemdisj  7940  suplocexprlemub  7943  0r  7970  1sr  7971  m1r  7972  m1p1sr  7980  m1m1sr  7981  0lt1sr  7985  1ne0sr  7986  1idsr  7988  recexgt0sr  7993  prsradd  8006  caucvgsrlemoffres  8020  caucvgsr  8022  mappsrprg  8024  map2psrprg  8025  pitonnlem1p1  8066  pitonnlem2  8067  pitoregt0  8069  peano2nnnn  8073  axi2m1  8095  axprecex  8100  axcnre  8101  nnindnn  8113  nntopi  8114  0cn  8171  addcli  8183  mulcli  8184  mulcomi  8185  readdcli  8192  remulcli  8193  rexpssxrxp  8224  ltrelxr  8240  gtneii  8275  lttri3i  8277  letri3i  8278  ltnsymi  8279  lenlti  8280  ltlei  8281  mulgt0i  8289  mulgt0ii  8290  0lt1  8306  addcomi  8323  pncan3oi  8395  resubcli  8442  subcli  8455  pncan3i  8456  negsubi  8457  subnegi  8458  subeq0i  8459  neg11i  8460  negcon1i  8461  negcon2i  8462  mulneg1i  8583  mulneg2i  8584  mul2negi  8585  addgt0ii  8671  ltnegi  8673  lenegi  8674  ltnegcon2i  8675  lesub0i  8676  ltaddposi  8677  posdifi  8678  ltnegcon1i  8679  lenegcon1i  8680  subge0i  8681  1ap0  8770  ltapii  8815  recrecapi  8924  dividapi  8925  div0api  8926  rec11apii  8941  divdiv32api  8947  recgt0ii  9087  ltrecii  9098  ltdiv23ii  9107  sup3exmid  9137  nnssre  9147  nnind  9159  nnmulcli  9165  nnsubi  9183  0le2  9233  1lt3  9315  2lt4  9317  1lt4  9318  3lt5  9320  2lt5  9321  1lt5  9322  4lt6  9324  3lt6  9325  2lt6  9326  1lt6  9327  5lt7  9329  4lt7  9330  3lt7  9331  2lt7  9332  1lt7  9333  6lt8  9335  5lt8  9336  4lt8  9337  3lt8  9338  2lt8  9339  1lt8  9340  7lt9  9342  6lt9  9343  5lt9  9344  4lt9  9345  3lt9  9346  2lt9  9347  1lt9  9348  2muline0  9369  nn0addcli  9439  nn0mulcli  9440  nn0addge1i  9450  nn0addge2i  9451  dfz2  9552  halfnz  9576  9p1e10  9613  numnncl  9620  numltc  9636  le9lt10  9637  nummac  9655  8lt10  9742  7lt10  9743  6lt10  9744  5lt10  9745  4lt10  9746  3lt10  9747  2lt10  9748  1lt10  9749  eluzaddi  9783  eluzsubi  9784  uzuzle23  9796  uzuzle24  9797  uzuzle34  9798  eluz2nn  9800  eluz4eluz2  9802  eluzge3nn  9806  divfnzn  9855  elq  9856  qreccl  9876  xrltnr  10014  mnfltpnf  10020  xaddmnf1  10083  pnfaddmnf  10085  mnfaddpnf  10086  xrex  10091  xaddid1  10097  xsubge0  10116  xposdif  10117  xleaddadd  10122  elicc2i  10174  ioomax  10183  iccmax  10184  ioopos  10185  elxrge0  10213  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  unitssre  10240  fz10  10281  fzpreddisj  10306  fz0to4untppr  10359  dfrp2  10524  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  frecfzennn  10689  xnn0nnen  10700  fnn0nninf  10701  fxnn0nninf  10702  0tonninf  10703  1tonninf  10704  m1expcl2  10824  m1expcl  10825  nn0expcli  10828  sqmuli  10885  cu2  10901  i3  10904  subsqi  10912  binom2subi  10918  bcpasc  11029  4bc2eq6  11037  hashinfom  11041  prhash2ex  11074  hashp1i  11075  lsw0g  11166  swrdccat3blem  11324  rei  11477  imi  11478  readdi  11506  imaddi  11507  remuli  11508  immuli  11509  cjaddi  11510  cjmuli  11511  ipcni  11512  crrei  11514  crimi  11515  rexfiuz  11567  sqrt1  11624  sqrt4  11625  sqrt9  11626  abs1  11650  sqrtmulii  11712  abslti  11716  abslei  11717  abssubi  11728  absmuli  11729  sqabsaddi  11730  sqabssubi  11731  abstrii  11733  fimaxre2  11805  climz  11870  abscn2  11893  recn2  11895  imcn2  11896  climabs  11898  climre  11900  climim  11901  fsumcnv  12016  fsumrelem  12050  fsumre  12051  fsumim  12052  arisum2  12078  expcnv  12083  geo2sum2  12094  geo2lim  12095  0.999...  12100  geoihalfsum  12101  fprodcnv  12204  fprodge0  12216  fprodge1  12218  ege2le3  12250  ef0  12251  reeff1  12279  tan0  12310  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  cos1bnd  12338  cos2bnd  12339  sinltxirr  12340  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  sincos1sgn  12344  sincos2sgn  12345  cos12dec  12347  egt2lt3  12359  epos  12360  ene1  12364  eap1  12365  3dvds  12443  3dvdsdec  12444  3dvds2dec  12445  odd2np1lem  12451  n2dvds1  12491  z4even  12495  ndvdsi  12512  flodddiv4  12515  bitsp1o  12532  0bits  12538  gcd0val  12549  6gcd4e2  12584  3lcm2e6woprm  12676  6lcm4e12  12677  3lcm2e6  12750  sqrt2irrlem  12751  phimullem  12815  pockthi  12949  4sqlem19  13000  dec2dvds  13002  dec5dvds2  13004  dec2nprm  13006  modxai  13007  gcdi  13011  gcdmodi  13012  numexpp1  13015  karatsuba  13021  2exp7  13025  xpnnen  13033  xpomen  13034  ennnfonelemj0  13040  ennnfonelem0  13044  ennnfonelemhf1o  13052  exmidunben  13065  qnnen  13070  unct  13081  setscom  13140  strleun  13205  prdsex  13370  prdsvallem  13373  imasival  13407  ismgm  13458  fn0g  13476  fngsum  13489  issgrp  13504  ismnddef  13519  isghm  13848  isrng  13966  rngmgpf  13969  isring  14032  mgpf  14043  dfrhm2  14187  rhmex  14190  isdomn  14302  rmodislmod  14384  lidlmex  14508  mopnset  14585  cnfldstr  14591  cnfldcj  14598  cnfld0  14604  cnfldplusf  14607  zringcrng  14625  zringmulr  14632  zringmpg  14639  znval  14669  psrval  14699  fnpsr  14700  fnmpl  14726  txtopi  15004  txunii  15007  upxp  15015  uptx  15017  cnmpt1st  15031  cnmpt2nd  15032  txswaphmeolem  15063  qtopbasss  15264  cnmet  15273  cnfldms  15279  cnopncntop  15287  cnopn  15288  remet  15291  blssioo  15296  tgqioo  15298  tgioo2cntop  15300  tgioo2  15302  divcnap  15308  abscncf  15328  recncf  15329  imcncf  15330  cjcncf  15331  mulc1cncf  15332  cncfcn1cntop  15337  idcncf  15344  cdivcncfap  15347  expcncf  15352  cnrehmeocntop  15353  maxcncf  15358  mincncf  15359  ivthreinc  15388  hovercncf  15389  limccnp2lem  15419  limccnp2cntop  15420  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvrecap  15456  dveflem  15469  dvef  15470  sincn  15512  coscn  15513  reeff1oleme  15515  reeff1o  15516  cosz12  15523  sin0pilem1  15524  sin0pilem2  15525  pipos  15531  sinhalfpilem  15534  sincosq1lem  15568  sincosq1sgn  15569  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  cosq14gt0  15575  cosq23lt0  15576  coseq0q4123  15577  coseq00topi  15578  coseq0negpitopi  15579  tangtx  15581  sincos4thpi  15583  tan4thpi  15584  sincos6thpi  15585  pigt3  15587  cosordlem  15592  cosq34lt1  15593  cos02pilt1  15594  cos0pilt1  15595  ioocosf1o  15597  negpitopissre  15598  log1  15609  loge  15610  2logb9irr  15714  sqrt2cxp2logb9e3  15718  2logb9irrap  15720  mpodvdsmulf1o  15733  fsumdvdsmul  15734  1sgm2ppw  15738  lgsdir2lem2  15777  lgsdir2lem3  15778  lgseisenlem4  15821  2lgsoddprmlem3  15859  2sqlem9  15872  2sqlem10  15873  opvtxfvi  15897  opiedgfvi  15898  umgrbien  15980  usgrprc  16122  vtxdfifiun  16167  upgr2wlkdc  16247  konigsbergvtx  16352  konigsbergiedg  16353  konigsbergumgr  16357  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem5  16362  konigsberg  16363  ex-fl  16368  ex-ceil  16369  ex-bc  16372  ex-dvds  16373  ex-gcd  16374  bj-charfunbi  16457  bj-unex  16565  bj-nn0suc0  16596  bj-nntrans  16597  bj-nnelirr  16599  012of  16643  2o01f  16644  pwle2  16650  nnsf  16658  peano3nninf  16660  exmidsbthrlem  16677  sbthom  16681  isomninnlem  16685  iooref1o  16689  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  apdiff  16703  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  dceqnconst  16716  dcapnconst  16717  nconstwlpolemgt0  16720  taupi  16729