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  7295  oaabs2  7296  omabs  7298  undom  7607  sbthlem8  7636  findcard3  7765  cantnfle  8093  cantnfp1  8103  cantnflem1c  8109  cantnfleOLD  8123  cantnfp1OLD  8129  cantnflem1cOLD  8132  sornom  8660  enfin2i  8704  ttukeylem6  8897  fpwwe2lem13  9023  fpwwe2  9024  winalim2  9077  wuncval2  9128  xlemul1a  11491  difreicc  11663  flflp1  11926  faclbnd  12350  swrdswrd  12667  swrdccatin12lem3  12697  swrdccat3blem  12702  ello12  13321  lo1bdd2  13329  elo12  13332  rlimclim1  13350  rlimcld2  13383  o1co  13391  o1of2  13417  o1rlimmul  13423  rlimsqzlem  13453  isercoll  13472  o1fsum  13609  supcvg  13649  dvds2ln  13996  isprm5  14235  pcadd  14390  vdwlem2  14482  vdwlem11  14491  sbcie3s  14658  prdsval  14834  mreexexlem4d  15026  isacs2  15032  catcocl  15064  catass  15065  subccocl  15193  fullsubc  15198  funcco  15219  funcpropd  15248  fullpropd  15268  ffthiso  15277  isnat  15295  natpropd  15324  fucpropd  15325  xpcval  15425  evlf2  15466  curfpropd  15481  curfuncf  15486  uncfcurf  15487  curf2ndf  15495  hofcl  15507  hofpropd  15515  yonffthlem  15530  isacs3lem  15775  acsfiindd  15786  gsumpropd2lem  15879  resmhm2b  15971  mhmid  16170  mhmmnd  16171  ghmgrp  16173  conjnmzb  16280  pgpfi  16604  sylow3lem2  16627  efgredlem  16744  frgpnabllem1  16856  dprdfcntz  17028  dprdfcntzOLD  17034  ablfac1b  17100  pgpfac1lem3  17107  pgpfac1lem5  17109  pgpfaclem3  17113  islmhm2  17663  lspsneleq  17740  psrval  17990  psrass1  18039  resspsrmul  18051  mplbas2  18113  mplbas2OLD  18114  coe1tmmul  18297  gsummoncoe1  18325  znunit  18580  psgndiflemB  18614  uvcff  18800  uvcf1  18801  lindfmm  18840  dmatsubcl  18978  scmatscm  18993  smatvscl  19004  marrepval  19042  mdetdiaglem  19078  mdetunilem8  19099  mdetunilem9  19100  pmatcoe1fsupp  19180  decpmatmulsumfsupp  19252  pmatcollpw2lem  19256  mp2pm2mplem4  19288  pm2mpmhmlem1  19297  pm2mpmhmlem2  19298  pm2mp  19304  fvmptnn04if  19328  cpmadugsumfi  19356  cpmidg2sum  19359  cpmadumatpoly  19362  cayhamlem4  19367  neiptoptop  19610  neitr  19659  ordtrest2lem  19682  cnpnei  19743  iscncl  19748  cncls  19753  cnntr  19754  cncnp  19759  lmcnp  19783  isreg2  19856  hauscmplem  19884  cmpfi  19886  1stcfb  19924  1stcrest  19932  2ndcctbss  19934  2ndcomap  19937  islly2  19963  cldllycmp  19974  lly1stc  19975  locfincmp  20005  llycmpkgen2  20029  1stckgenlem  20032  kgencn2  20036  kgencn3  20037  ptbasfi  20060  ptpjopn  20091  txdis1cn  20114  txlly  20115  txnlly  20116  txtube  20119  txcmplem2  20121  tx1stc  20129  txkgen  20131  xkopt  20134  xkoco2cn  20137  xkococnlem  20138  xkococn  20139  xkoinjcn  20166  tgqtop  20191  regr1lem  20218  kqreglem1  20220  nrmhmph  20273  rnelfmlem  20431  rnelfm  20432  fmfnfmlem4  20436  fmfnfm  20437  ufldom  20441  flimopn  20454  hauspwpwf1  20466  fclsopn  20493  fclsnei  20498  fclsrest  20503  alexsublem  20522  alexsubALTlem3  20527  ptcmplem2  20531  ptcmplem3  20532  cnextfun  20542  cnextcn  20545  symgtgp  20578  tgpt0  20595  qustgpopn  20596  tsmsxplem1  20633  trust  20710  utopsnneiplem  20728  utop3cls  20732  utopreg  20733  isucn2  20760  cstucnd  20765  ucncn  20766  fmucnd  20773  cfilufg  20774  neipcfilu  20777  met2ndci  21003  prdsxmslem2  21010  metcnp3  21021  metustidOLD  21040  metustid  21041  metustexhalfOLD  21044  metustexhalf  21045  metustOLD  21048  metust  21049  metutopOLD  21063  psmetutop  21064  nmoleub  21216  reconnlem2  21310  xrge0tsms  21317  cncfco  21389  lebnumlem3  21441  lebnum  21442  nmoleub2lem2  21577  nmoleub3  21580  iscfil2  21683  iscau4  21696  iscmet3lem2  21709  equivcfil  21716  equivcau  21717  caubl  21724  rrxdstprj1  21814  ovolshftlem2  21899  ovolicc2lem4  21909  uniioombl  21976  i1fmulclem  22087  mbfi1fseqlem6  22105  itg2const2  22126  itg2split  22134  ellimc2  22259  ellimc3  22261  limcflf  22263  dvmptfsum  22354  dvferm1  22364  dvferm2  22366  dvlip2  22374  c1lip1  22376  lhop1  22393  ftc1a  22416  ply1divex  22515  plyeq0lem  22585  plymullem1  22589  coemullem  22625  coemulc  22630  ulmshftlem  22762  ulmcaulem  22767  ulmbdd  22771  ulmcn  22772  ulmdvlem3  22775  mtestbdd  22778  pserulm  22795  pserdvlem2  22801  abelthlem8  22812  xrlimcnp  23276  jensen  23296  logfac2  23470  dchrelbas3  23491  dchrpt  23520  lgsquad3  23614  2sqb  23631  rpvmasumlem  23650  dchrisumlem1  23652  dchrisumlem3  23654  dchrmusum2  23657  dchrvmasumlem2  23661  dchrisum0flblem1  23671  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0  23683  mulog2sumlem2  23698  pntlem3  23772  ostth3  23801  istrkgcb  23831  tgbtwndiff  23875  tgcgrxfr  23887  motcgrg  23909  lnext  23932  tgbtwnconn1  23940  tgbtwnconn3  23942  legval  23949  legtrid  23956  legso  23963  tglnne  23986  tglineeltr  23989  tglnne0  23998  colline  24008  tglowdim2l  24009  tglowdim2ln  24010  mirreu3  24013  mirbtwnhl  24038  krippenlem  24045  midexlem  24047  perpcom  24068  perpneq  24069  footex  24073  colperpexlem3  24084  colperpex  24085  opphllem  24087  midex  24089  opptgdim2  24095  oppnid  24096  opphllem2  24098  opphllem5  24101  opphllem6  24102  lnopp2hpgb  24110  hpgerlem  24112  lmieu  24128  f1otrg  24152  f1otrge  24153  axeuclidlem  24243  axcontlem2  24246  usgraidx2vlem2  24370  usgrares1  24388  nbgraf1olem5  24423  usgra2wlkspth  24599  constr3cycl  24639  clwlkisclwwlklem1  24765  wwlkext2clwwlk  24781  eupath2  24958  frisusgranb  24975  frgra2v  24977  frgra3vlem2  24979  2pthfrgrarn2  24988  2spotiundisj  25040  usg2spot2nb  25043  usgreghash2spotv  25044  numclwwlk2lem1  25080  isgrp2d  25215  ubthlem3  25766  chirredlem1  27287  chirredlem3  27289  cdj1i  27330  xrge0infss  27558  omndmul2  27680  submarchi  27708  gsumle  27748  xrge0tsmsd  27753  suborng  27783  isarchiofld  27785  fimaproj  27814  locfinreflem  27821  cmppcmp  27839  ordtrest2NEWlem  27882  ordtconlem1  27884  lmdvg  27913  esumpcvgval  28062  volmeas  28181  imambfm  28211  sgnmul  28459  signsply0  28486  signstres  28510  lgamucov  28558  erdszelem8  28620  pconcon  28654  cvmlift2lem12  28737  cvmlift3lem5  28746  cvmlift3lem7  28748  cvmlift3lem8  28749  mrsubrn  28851  msrval  28876  msubff1  28894  nodenselem5  29421  btwnconn1lem13  29725  ltflcei  30019  heicant  30025  mblfinlem2  30028  mblfinlem3  30029  mblfinlem4  30030  cnambfre  30039  itg2addnclem  30042  itg2addnclem2  30043  itg2gt0cn  30046  bddiblnc  30061  ftc1cnnc  30065  ftc1anclem5  30070  ftc1anclem7  30072  ftc1anc  30074  elicc3  30111  neibastop2lem  30154  equivtotbnd  30250  isbndx  30254  ssbnd  30260  heibor1lem  30281  rrncmslem  30304  elrfi  30602  eldioph2  30671  diophin  30682  irrapxlem2  30735  irrapxlem3  30736  irrapxlem4  30737  irrapxlem5  30738  pell1234qrne0  30765  pell1234qrreccl  30766  pell1234qrmulcl  30767  pell14qrgt0  30771  pell14qrdich  30781  pell1qrge1  30782  pellfundex  30798  congabseq  30888  jm2.27b  30924  jm2.27  30926  fnwe2lem2  30973  kelac1  30985  lnrfg  31044  hbt  31055  cntzsdrg  31127  cvgdvgrat  31170  lcmgcdlem  31188  mccl  31560  limcrecl  31589  lptioo2  31591  lptioo1  31592  lptre2pt  31600  addlimc  31608  icccncfext  31644  cncfiooicclem1  31650  cncfiooiccre  31652  dvbdfbdioolem2  31680  ioodvbdlimc1lem1  31682  dvnxpaek  31693  dvmptfprodlem  31695  dvmptfprod  31696  dvnprodlem3  31699  itgioocnicc  31730  itgspltprt  31732  stoweidlem31  31767  fourierdlem39  31882  fourierdlem42  31885  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem51  31894  fourierdlem64  31907  fourierdlem65  31908  fourierdlem74  31917  fourierdlem75  31918  fourierdlem81  31924  fourierdlem82  31925  fourierdlem101  31944  etransclem23  31994  etransclem27  31998  etransclem32  32003  etransclem33  32004  etransclem35  32006  etransclem38  32009  usgra2pthspth  32305  usgvad2edg  32365  resmgmhm2b  32442  2zrngmmgm  32579  cznrng  32590  rnghmsubcsetclem2  32659  rhmsubcsetclem2  32702  srhmsubc  32752  rhmsubclem4  32765  srhmsubcOLD  32771  rhmsubcOLDlem4  32784  lincsum  32900  lcoss  32907  snlindsntor  32942  islindeps2  32954  ad5ant12  33100  sineq0ALT  33605  islshpat  34617  lfl1dim  34721  lfl1dim2N  34722  lkrpssN  34763  glbconN  34976  hlhgt2  34988  3dim2  35067  3dim3  35068  islln3  35109  islvol5  35178  2lplnja  35218  dalem19  35281  isline4N  35376  2polssN  35514  lhpmatb  35630  4atex  35675  trlatn0  35772  cdlemf2  36163  dialss  36648  diaglbN  36657  diaintclN  36660  dibglbN  36768  dibintclN  36769  dihlsscpre  36836  dihglblem5aN  36894  dihglblem2aN  36895  dihglblem4  36899  dihatexv  36940  dihjat1lem  37030  lcfl6  37102  mapdval2N  37232
  Copyright terms: Public domain W3C validator