Theorem mp3an 1424

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
mp3an.1	|- ph
mp3an.2	|- ps
mp3an.3	|- ch
mp3an.4	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an	|- th

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 |- ps
2		mp3an.3	. 2 |- ch
3		mp3an.1	. . 3 |- ph
4		mp3an.4	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
5	3, 4	mp3an1 1411	. 2 |- ( ( ps /\ ch ) -> th )
6	1, 2, 5	mp2an 708	1 |- th

Syntax hints:   -> wi 4   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  vtocl3  3262  raltp  4240  rextp  4241  funopg  5922  feq12i  6038  ftp  6424  caovass  6834  caovdi  6853  ordom  7074  ofmres  7164  omopthlem1  7735  omopthlem2  7736  omopthi  7737  xpcomen  8051  unfilem3  8226  hartogs  8449  card2on  8459  unwf  8673  tskwe  8776  alephsmo  8925  dfac4  8945  dfac2a  8952  ackbij1lem5  9046  ackbij1lem13  9054  axdc2lem  9270  axcclem  9279  ondomon  9385  cfpwsdom  9406  pwfseqlem2  9481  pwfseqlem3  9482  1lt2pi  9727  addassi  10048  mulassi  10049  adddii  10050  adddiri  10051  lttri  10163  lelttri  10164  ltletri  10165  letri  10166  ltadd2i  10168  mul02lem2  10213  addid1  10216  addcani  10229  addcan2i  10230  mul12i  10231  mul32i  10232  add12i  10258  add32i  10259  subaddi  10368  subadd2i  10369  subsub23i  10371  addsubassi  10372  addsubi  10373  subcani  10374  subcan2i  10375  pnncani  10376  subdii  10479  subdiri  10480  ltadd1i  10582  leadd1i  10583  leadd2i  10584  ltsubaddi  10585  lesubaddi  10586  ltsubadd2i  10587  lesubadd2i  10588  ltaddsubi  10589  mulcani  10666  div23i  10783  div11i  10784  1mhlfehlf  11251  halfpm6th  11253  3halfnz  11456  addex  11830  mulex  11831  unirnioo  12273  ioorebas  12275  xnn0xrge0  12325  fldiv4lem1div2  12638  uzenom  12763  nnenom  12779  m1expcl2  12882  i4  12967  expnass  12970  faclbnd4lem1  13080  bcn1  13100  hashfxnn0  13124  cats1fvn  13603  cats1fv  13604  cats1cat  13606  cats2cat  13607  wrdlen3s3  13692  abs3difi  14148  0.999...  14612  0.999...OLD  14613  geoihalfsum  14614  bpoly3  14789  ef01bndlem  14914  cos1bnd  14917  cos2bnd  14918  sin4lt0  14925  rpnnen2lem3  14945  rpnnen2lem11  14953  rpnnen  14956  rexpen  14957  aleph1irr  14975  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  divalglem2  15118  ndvdsi  15136  flodddiv4  15137  gcdaddmlem  15245  bezout  15260  3lcm2e6woprm  15328  6lcm4e12  15329  lcmf0  15347  lcmf2a3a4e12  15360  3prm  15406  dec2dvds  15767  modxai  15772  modsubi  15776  gcdi  15777  numexp2x  15783  prdsval  16115  prdsds  16124  mreexexdOLD  16309  plusffval  17247  pmtrprfval  17907  m1expaddsub  17918  0frgp  18192  staffval  18847  scaffval  18881  cnfldcj  19753  cnfldds  19756  cnfldfun  19758  xrsadd  19763  xrsmul  19764  xrsds  19789  cnmgpid  19808  nn0srg  19816  rge0srg  19817  zring0  19828  cnmsgnsubg  19923  psgninv  19928  re0g  19958  ipffval  19993  ocvfval  20010  frlmbas  20099  mdetrlin  20408  mdetunilem9  20426  leordtval2  21016  iscnp2  21043  utop3cls  22055  nmfval  22393  nmoffn  22515  nmofval  22518  icccld  22570  addcnlem  22667  iimulcn  22737  icopnfhmeo  22742  iccpnfcnv  22743  iccpnfhmeo  22744  xrhmeo  22745  xrhmph  22746  oprpiece1res1  22750  oprpiece1res2  22751  ishtpy  22771  pcoass  22824  cnstrcvs  22941  cncvs  22945  recvs  22946  qcvs  22947  zclmncvs  22948  tchex  23016  cnfldcusp  23153  resscdrg  23154  reust  23169  recusp  23170  vitalilem4  23380  vitalilem5  23381  mbfdm  23395  dveflem  23742  dvlipcn  23757  c1lip2  23761  dgrid  24020  iaa  24080  abelthlem3  24187  abelthlem5  24189  abelth  24195  efcn  24197  sinhalfpilem  24215  sincosq1lem  24249  sincosq4sgn  24253  tangtx  24257  sincos4thpi  24265  sincos6thpi  24267  pige3  24269  relogcn  24384  dvlog2lem  24398  dvlog2  24399  logtayl  24406  logtayl2  24408  cxpsqrtlem  24448  cxpsqrt  24449  cxpcn2  24487  cxpcn3  24489  logblog  24530  ang180lem1  24539  ang180lem2  24540  1cubrlem  24568  mcubic  24574  quart1lem  24582  quart1  24583  reasinsin  24623  atancj  24637  efiatan  24639  atantan  24650  atanbndlem  24652  atan1  24655  atancn  24663  atantayl2  24665  log2cnv  24671  log2tlbnd  24672  log2ublem1  24673  log2ublem2  24674  log2ub  24676  efrlim  24696  scvxcvx  24712  1sgm2ppw  24925  ppiub  24929  bclbnd  25005  bposlem8  25016  lgsdir2lem1  25050  lgsdir2lem5  25054  lgseisenlem1  25100  lgseisenlem2  25101  lgsquadlem1  25105  chebbnd1  25161  dchrvmasumlem2  25187  istrkg3ld  25360  trgcgrg  25410  ax5seglem7  25815  axlowdimlem6  25827  axlowdimlem8  25829  axlowdimlem11  25832  cusgrsizeindb1  26346  vtxdginducedm1  26439  0grrusgr  26475  erclwwlkstr  26936  erclwwlksntr  26948  wlk2v2e  27017  upgr3v3e3cycl  27040  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  konigsberglem5  27118  ex-fl  27304  ex-mod  27306  ex-hash  27310  ex-lcm  27315  0vfval  27461  smcnlem  27552  lnocoi  27612  nmlno0lem  27648  nmblolbii  27654  blocnilem  27659  blocni  27660  cncph  27674  isph  27677  ip0i  27680  ip1ilem  27681  ip2i  27683  ipdirilem  27684  ipasslem7  27691  ipasslem8  27692  ipasslem9  27693  ipasslem10  27694  ipasslem11  27695  ip2dii  27699  pythi  27705  siilem1  27706  siilem2  27707  siii  27708  hvmulassi  27903  hvmulcomi  27904  hvdistr1i  27908  hvsubdistr1i  27909  hvassi  27910  hvadd32i  27911  hvsubassi  27912  hvsub32i  27913  normlem0  27966  normlem8  27974  normlem9  27975  bcseqi  27977  polid2i  28014  hhph  28035  hlim0  28092  shscli  28176  shlessi  28236  shlej1i  28237  omlsilem  28261  shlubi  28274  h1de2i  28412  pjadjii  28533  pjaddii  28534  pjmulii  28536  pjdifnormii  28542  pjcji  28543  hoaddsubassi  28679  eigrei  28693  eigposi  28695  eigorthi  28696  adj0  28853  lnopeq0lem1  28864  lnopunilem1  28869  lnophmlem2  28876  nmcexi  28885  nmcopexi  28886  lnfn0i  28901  nmcfnexi  28910  mdexchi  29194  xppreima2  29450  dp2clq  29588  dp2lt  29592  dp2ltc  29594  dpexpp1  29616  dpmul  29621  dpmul4  29622  elxrge02  29640  xrge0adddir  29692  xrnarchi  29738  xrge0slmod  29844  psgnid  29847  raddcn  29975  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhmeo  29982  xrge0iifhom  29983  xrge0iifmhm  29985  xrge0mulc1cn  29987  lmlimxrge0  29994  pnfneige0  29997  lmxrge0  29998  zringnm  30004  rezh  30015  qqh0  30028  qqh1  30029  qqhucn  30036  esumpinfval  30135  hashf2  30146  esumcvg  30148  br2base  30331  sxbrsigalem3  30334  dya2iocbrsiga  30337  dya2icobrsiga  30338  sxbrsigalem1  30347  sxbrsigalem2  30348  sxbrsigalem4  30349  sxbrsigalem5  30350  sxbrsiga  30352  ballotlem2  30550  ballotlem4  30560  ballotlemi1  30564  ballotth  30599  sgnclre  30601  signstf  30643  itgexpif  30684  chtvalz  30707  hgt750lemd  30726  hgt750lem  30729  tgoldbachgnn  30737  subfacp1lem1  31161  subfacp1lem6  31167  kur14lem6  31193  cvmliftlem4  31270  problem4  31562  quad3  31564  logi  31620  iexpire  31621  fununiq  31667  fvtransport  32139  bj-minftyccb  33112  taupilem2  33168  1oequni2o  33216  finxp1o  33229  finxpreclem4  33231  cos2h  33400  tan2h  33401  pigt3  33402  poimirlem9  33418  poimirlem27  33436  poimirlem28  33437  ismblfin  33450  mbfposadd  33457  ftc1anclem5  33489  asindmre  33495  dvasin  33496  dvacos  33497  rrnval  33626  el3v  33987  dihjatcclem4  36710  rabren3dioph  37379  jm2.27dlem2  37577  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  expdioph  37590  arearect  37801  areaquad  37802  corclrcl  37999  iunrelexpuztr  38011  corcltrcl  38031  dffrege76  38233  k0004val0  38452  lhe4.4ex1a  38528  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  ax6e2ndeqALT  39167  sineq0ALT  39173  pnfel0pnf  39754  lptioo2cn  39877  limsup10ex  40005  liminf10ex  40006  icccncfext  40100  itgsin0pilem1  40165  itgsbtaddcnst  40198  stoweidlem13  40230  wallispilem2  40283  wallispilem4  40285  wallispi2lem1  40288  stirlinglem13  40303  dirkerper  40313  dirkertrigeqlem3  40317  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem4  40323  fourierdlem42  40366  fourierdlem62  40385  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  sqwvfoura  40445  fourierswlem  40447  fouriersw  40448  smfmullem4  41001  fmtnoprmfac2lem1  41478  fmtno4prm  41487  2exp5  41507  2exp11  41517  3exp4mod41  41533  41prothprmlem2  41535  6gbe  41659  7gbow  41660  8gbe  41661  9gbo  41662  11gbo  41663  sbgoldbalt  41669  nnsum4primesevenALTV  41689  0nodd  41810  oddinmgm  41815  2zrng0  41938  zlmodzxz0  42134  zlmodzxzequa  42285  zlmodzxzequap  42288  zlmodzxzldeplem3  42291  nnlog2ge0lt1  42360  blen1  42378  blen2  42379  nnolog2flm1  42384