MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad3antrrr Structured version   Unicode version

Theorem ad3antrrr 729
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad3antrrr  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem ad3antrrr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 465 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 725 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  ad4antr  731  oaabs  7183  oaabs2  7184  omabs  7186  undom  7499  sbthlem8  7528  findcard3  7656  cantnfle  7980  cantnfp1  7990  cantnflem1c  7996  cantnfleOLD  8010  cantnfp1OLD  8016  cantnflem1cOLD  8019  sornom  8547  enfin2i  8591  ttukeylem6  8784  fpwwe2lem13  8910  fpwwe2  8911  winalim2  8964  wuncval2  9015  xlemul1a  11352  difreicc  11518  faclbnd  12167  swrdswrd  12456  swrdccatin12lem3  12483  swrdccat3blem  12488  ello12  13096  lo1bdd2  13104  elo12  13107  rlimclim1  13125  rlimcld2  13158  o1co  13166  o1of2  13192  o1rlimmul  13198  rlimsqzlem  13228  isercoll  13247  o1fsum  13378  supcvg  13420  dvds2ln  13665  isprm5  13900  pcadd  14053  vdwlem2  14145  vdwlem11  14154  sbcie3s  14320  prdsval  14495  mreexexlem4d  14687  isacs2  14693  catcocl  14725  catass  14726  subccocl  14857  fullsubc  14862  funcco  14883  funcpropd  14912  fullpropd  14932  ffthiso  14941  isnat  14959  natpropd  14988  fucpropd  14989  xpcval  15089  evlf2  15130  curfpropd  15145  curfuncf  15150  uncfcurf  15151  curf2ndf  15159  hofcl  15171  hofpropd  15179  yonffthlem  15194  isacs3lem  15438  acsfiindd  15449  resmhm2b  15591  gsumpropd2lem  15607  conjnmzb  15883  pgpfi  16208  sylow3lem2  16231  efgredlem  16348  frgpnabllem1  16455  dprdfcntz  16604  dprdfcntzOLD  16610  ablfac1b  16676  pgpfac1lem3  16683  pgpfac1lem5  16685  pgpfaclem3  16689  islmhm2  17225  lspsneleq  17302  psrval  17535  psrass1  17584  resspsrmul  17596  mplbas2  17658  mplbas2OLD  17659  coe1tmmul  17838  znunit  18105  psgndiflemB  18139  uvcff  18325  uvcf1  18326  lindfmm  18365  marrepval  18484  mdetdiaglem  18520  mdetunilem8  18541  mdetunilem9  18542  neiptoptop  18851  neitr  18900  ordtrest2lem  18923  cnpnei  18984  iscncl  18989  cncls  18994  cnntr  18995  cncnp  19000  lmcnp  19024  isreg2  19097  hauscmplem  19125  cmpfi  19127  1stcfb  19165  1stcrest  19173  2ndcctbss  19175  2ndcomap  19178  islly2  19204  cldllycmp  19215  lly1stc  19216  llycmpkgen2  19239  1stckgenlem  19242  kgencn2  19246  kgencn3  19247  ptbasfi  19270  ptpjopn  19301  txdis1cn  19324  txlly  19325  txnlly  19326  txtube  19329  txcmplem2  19331  tx1stc  19339  txkgen  19341  xkopt  19344  xkoco2cn  19347  xkococnlem  19348  xkococn  19349  xkoinjcn  19376  tgqtop  19401  regr1lem  19428  kqreglem1  19430  nrmhmph  19483  rnelfmlem  19641  rnelfm  19642  fmfnfmlem4  19646  fmfnfm  19647  ufldom  19651  flimopn  19664  hauspwpwf1  19676  fclsopn  19703  fclsnei  19708  fclsrest  19713  alexsublem  19732  alexsubALTlem3  19737  ptcmplem2  19741  ptcmplem3  19742  cnextfun  19752  cnextcn  19755  symgtgp  19788  tgpt0  19805  divstgpopn  19806  tsmsxplem1  19843  trust  19920  utopsnneiplem  19938  utop3cls  19942  utopreg  19943  isucn2  19970  cstucnd  19975  ucncn  19976  fmucnd  19983  cfilufg  19984  neipcfilu  19987  met2ndci  20213  prdsxmslem2  20220  metcnp3  20231  metustidOLD  20250  metustid  20251  metustexhalfOLD  20254  metustexhalf  20255  metustOLD  20258  metust  20259  metutopOLD  20273  psmetutop  20274  nmoleub  20426  reconnlem2  20520  xrge0tsms  20527  cncfco  20599  lebnumlem3  20651  lebnum  20652  nmoleub2lem2  20787  nmoleub3  20790  iscfil2  20893  iscau4  20906  iscmet3lem2  20919  equivcfil  20926  equivcau  20927  caubl  20934  rrxdstprj1  21024  ovolshftlem2  21109  ovolicc2lem4  21119  uniioombl  21185  i1fmulclem  21296  mbfi1fseqlem6  21314  itg2const2  21335  itg2split  21343  ellimc2  21468  ellimc3  21470  limcflf  21472  dvmptfsum  21563  dvferm1  21573  dvferm2  21575  dvlip2  21583  c1lip1  21585  lhop1  21602  ftc1a  21625  ply1divex  21724  plyeq0lem  21794  plymullem1  21798  coemullem  21833  coemulc  21838  ulmshftlem  21970  ulmcaulem  21975  ulmbdd  21979  ulmcn  21980  ulmdvlem3  21983  mtestbdd  21986  pserulm  22003  pserdvlem2  22009  abelthlem8  22020  xrlimcnp  22478  jensen  22498  logfac2  22672  dchrelbas3  22693  dchrpt  22722  lgsquad3  22816  2sqb  22833  rpvmasumlem  22852  dchrisumlem1  22854  dchrisumlem3  22856  dchrmusum2  22859  dchrvmasumlem2  22863  dchrisum0flblem1  22873  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0  22885  mulog2sumlem2  22900  pntlem3  22974  ostth3  23003  istrkgcb  23033  tgbtwndiff  23077  tgcgrxfr  23089  lnext  23119  tgbtwnconn1  23127  tgbtwnconn3  23129  legval  23136  legtrid  23143  tglnne  23156  tglineeltr  23159  colline  23177  tglowdim2l  23178  tglowdim2ln  23179  mirreu3  23184  krippenlem  23210  midexlem  23212  perpcom  23232  perpneq  23233  footex  23237  colperplem3  23242  colperp  23243  mideulem  23244  mideu  23245  f1otrg  23252  f1otrge  23253  axeuclidlem  23343  axcontlem2  23346  usgraidx2vlem2  23445  usgrares1  23458  nbgraf1olem5  23489  constr3cycl  23682  eupath2  23736  isgrp2d  23857  ubthlem3  24408  chirredlem1  25929  chirredlem3  25931  cdj1i  25972  xrge0infss  26187  omndmul2  26309  submarchi  26337  gsumle  26380  xrge0tsmsd  26387  suborng  26417  isarchiofld  26419  ordtrest2NEWlem  26486  ordtconlem1  26488  lmdvg  26517  esumpcvgval  26661  volmeas  26781  imambfm  26811  sgnmul  27059  signsply0  27086  signstres  27110  lgamucov  27158  erdszelem8  27220  pconcon  27254  cvmlift2lem12  27337  cvmlift3lem5  27346  cvmlift3lem7  27348  cvmlift3lem8  27349  nodenselem5  27960  btwnconn1lem13  28264  ltflcei  28557  lxflflp1  28559  heicant  28564  mblfinlem2  28567  mblfinlem3  28568  mblfinlem4  28569  cnambfre  28578  itg2addnclem  28581  itg2addnclem2  28582  itg2gt0cn  28585  bddiblnc  28600  ftc1cnnc  28604  ftc1anclem5  28609  ftc1anclem7  28611  ftc1anc  28613  elicc3  28650  locfincmp  28714  neibastop2lem  28719  sstotbnd2  28811  equivtotbnd  28815  isbndx  28819  ssbnd  28825  heibor1lem  28846  rrncmslem  28869  elrfi  29168  eldioph2  29238  diophin  29249  irrapxlem2  29302  irrapxlem3  29303  irrapxlem4  29304  irrapxlem5  29305  pell1234qrne0  29332  pell1234qrreccl  29333  pell1234qrmulcl  29334  pell14qrgt0  29338  pell1234qrdich  29340  pell14qrdich  29348  pell1qrge1  29349  pellfundex  29365  congabseq  29455  jm2.27b  29493  jm2.27  29495  fnwe2lem2  29542  kelac1  29554  lnrfg  29613  hbt  29624  cntzsdrg  29697  stoweidlem31  29964  usgra2pthspth  30433  usgra2wlkspth  30436  clwlkisclwwlklem1  30587  wwlkext2clwwlk  30603  frisusgranb  30727  frgra2v  30729  frgra3vlem2  30731  2pthfrgrarn2  30740  usg2spot2nb  30796  usgreghash2spotv  30797  numclwwlk2lem1  30833  gsummoncoe1  30985  dmatsubcl  31031  lincsum  31070  lcoss  31077  snlindsntor  31112  islindeps2  31124  pmatcoe1fsupp  31167  pmatcollpw1dst  31228  pmatcollpwlem  31233  mp2pm2mplem4  31264  pmattomply1mhmlem1  31273  pmattomply1mhmlem2  31274  pmat2matp  31279  fvmptnn04if  31303  cpmidpmatlem3  31326  cpmadugsumfi  31331  cpmidg2sum  31334  cpmadumatpoly  31338  cayhamlem4  31343  ad5ant12  31467  sineq0ALT  31973  islshpat  32968  lfl1dim  33072  lfl1dim2N  33073  lkrpssN  33114  glbconN  33327  hlhgt2  33339  3dim2  33418  3dim3  33419  islln3  33460  islvol5  33529  2lplnja  33569  dalem19  33632  isline4N  33727  2polssN  33865  lhpmatb  33981  4atex  34026  trlatn0  34122  cdlemf2  34512  dialss  34997  diaglbN  35006  diaintclN  35009  dibglbN  35117  dibintclN  35118  dihlsscpre  35185  dihglblem5aN  35243  dihglblem2aN  35244  dihglblem4  35248  dihatexv  35289  dihjat1lem  35379  lcfl6  35451  mapdval2N  35581
  Copyright terms: Public domain W3C validator