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

Theorem ad3antrrr 727
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 463 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 723 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ad4antr  729  oaabs  7211  oaabs2  7212  omabs  7214  undom  7524  sbthlem8  7553  findcard3  7678  cantnfle  8003  cantnfp1  8013  cantnflem1c  8019  cantnfleOLD  8033  cantnfp1OLD  8039  cantnflem1cOLD  8042  sornom  8570  enfin2i  8614  ttukeylem6  8807  fpwwe2lem13  8931  fpwwe2  8932  winalim2  8985  wuncval2  9036  xlemul1a  11401  difreicc  11573  flflp1  11843  faclbnd  12270  swrdswrd  12596  swrdccatin12lem3  12626  swrdccat3blem  12631  ello12  13341  lo1bdd2  13349  elo12  13352  rlimclim1  13370  rlimcld2  13403  o1co  13411  o1of2  13437  o1rlimmul  13443  rlimsqzlem  13473  isercoll  13492  o1fsum  13629  supcvg  13669  dvds2ln  14016  isprm5  14255  pcadd  14410  vdwlem2  14502  vdwlem11  14511  sbcie3s  14680  prdsval  14862  mreexexlem4d  15054  isacs2  15060  catcocl  15092  catass  15093  subccocl  15251  fullsubc  15256  funcco  15277  funcpropd  15306  fullpropd  15326  ffthiso  15335  isnat  15353  natpropd  15382  fucpropd  15383  xpcval  15563  evlf2  15604  curfpropd  15619  curfuncf  15624  uncfcurf  15625  curf2ndf  15633  hofcl  15645  hofpropd  15653  yonffthlem  15668  isacs3lem  15913  acsfiindd  15924  gsumpropd2lem  16017  resmhm2b  16109  mhmid  16308  mhmmnd  16309  ghmgrp  16311  conjnmzb  16418  pgpfi  16742  sylow3lem2  16765  efgredlem  16882  frgpnabllem1  16994  dprdfcntz  17162  dprdfcntzOLD  17168  ablfac1b  17234  pgpfac1lem3  17241  pgpfac1lem5  17243  pgpfaclem3  17247  islmhm2  17797  lspsneleq  17874  psrval  18124  psrass1  18173  resspsrmul  18185  mplbas2  18247  mplbas2OLD  18248  coe1tmmul  18431  gsummoncoe1  18459  znunit  18693  psgndiflemB  18727  uvcff  18911  uvcf1  18912  lindfmm  18947  dmatsubcl  19085  scmatscm  19100  smatvscl  19111  marrepval  19149  mdetdiaglem  19185  mdetunilem8  19206  mdetunilem9  19207  pmatcoe1fsupp  19287  decpmatmulsumfsupp  19359  pmatcollpw2lem  19363  mp2pm2mplem4  19395  pm2mpmhmlem1  19404  pm2mpmhmlem2  19405  pm2mp  19411  fvmptnn04if  19435  cpmadugsumfi  19463  cpmidg2sum  19466  cpmadumatpoly  19469  cayhamlem4  19474  neiptoptop  19718  neitr  19767  ordtrest2lem  19790  cnpnei  19851  iscncl  19856  cncls  19861  cnntr  19862  cncnp  19867  lmcnp  19891  isreg2  19964  hauscmplem  19992  cmpfi  19994  1stcfb  20031  1stcrest  20039  2ndcctbss  20041  2ndcomap  20044  islly2  20070  cldllycmp  20081  lly1stc  20082  locfincmp  20112  llycmpkgen2  20136  1stckgenlem  20139  kgencn2  20143  kgencn3  20144  ptbasfi  20167  ptpjopn  20198  txdis1cn  20221  txlly  20222  txnlly  20223  txtube  20226  txcmplem2  20228  tx1stc  20236  txkgen  20238  xkopt  20241  xkoco2cn  20244  xkococnlem  20245  xkococn  20246  xkoinjcn  20273  tgqtop  20298  regr1lem  20325  kqreglem1  20327  nrmhmph  20380  rnelfmlem  20538  rnelfm  20539  fmfnfmlem4  20543  fmfnfm  20544  ufldom  20548  flimopn  20561  hauspwpwf1  20573  fclsopn  20600  fclsnei  20605  fclsrest  20610  alexsublem  20629  alexsubALTlem3  20634  ptcmplem2  20638  ptcmplem3  20639  cnextfun  20649  cnextcn  20652  symgtgp  20685  tgpt0  20702  qustgpopn  20703  tsmsxplem1  20740  trust  20817  utopsnneiplem  20835  utop3cls  20839  utopreg  20840  isucn2  20867  cstucnd  20872  ucncn  20873  fmucnd  20880  cfilufg  20881  neipcfilu  20884  met2ndci  21110  prdsxmslem2  21117  metcnp3  21128  metustidOLD  21147  metustid  21148  metustexhalfOLD  21151  metustexhalf  21152  metustOLD  21155  metust  21156  metutopOLD  21170  psmetutop  21171  nmoleub  21323  reconnlem2  21417  xrge0tsms  21424  cncfco  21496  lebnumlem3  21548  lebnum  21549  nmoleub2lem2  21684  nmoleub3  21687  iscfil2  21790  iscau4  21803  iscmet3lem2  21816  equivcfil  21823  equivcau  21824  caubl  21831  rrxdstprj1  21921  ovolshftlem2  22006  ovolicc2lem4  22016  uniioombl  22083  i1fmulclem  22194  mbfi1fseqlem6  22212  itg2const2  22233  itg2split  22241  ellimc2  22366  ellimc3  22368  limcflf  22370  dvmptfsum  22461  dvferm1  22471  dvferm2  22473  dvlip2  22481  c1lip1  22483  lhop1  22500  ftc1a  22523  ply1divex  22622  plyeq0lem  22692  plymullem1  22696  coemullem  22732  coemulc  22737  ulmshftlem  22869  ulmcaulem  22874  ulmbdd  22878  ulmcn  22879  ulmdvlem3  22882  mtestbdd  22885  pserulm  22902  pserdvlem2  22908  abelthlem8  22919  xrlimcnp  23415  jensen  23435  logfac2  23609  dchrelbas3  23630  dchrpt  23659  lgsquad3  23753  2sqb  23770  rpvmasumlem  23789  dchrisumlem1  23791  dchrisumlem3  23793  dchrmusum2  23796  dchrvmasumlem2  23800  dchrisum0flblem1  23810  dchrisum0lem1b  23817  dchrisum0lem1  23818  dchrisum0  23822  mulog2sumlem2  23837  pntlem3  23911  ostth3  23940  istrkgcb  23970  tgbtwndiff  24017  tgcgrxfr  24029  motcgrg  24051  lnext  24074  tgbtwnconn1  24082  tgbtwnconn3  24084  legval  24091  legtrid  24098  legso  24105  tglnne  24128  tglineeltr  24131  tglnne0  24140  colline  24150  tglowdim2l  24151  tglowdim2ln  24152  mirreu3  24155  mirbtwnhl  24180  krippenlem  24187  midexlem  24189  perpcom  24210  perpneq  24211  footex  24215  colperpexlem3  24226  colperpex  24227  opphllem  24229  midex  24231  opptgdim2  24237  oppnid  24238  opphllem2  24240  opphllem5  24243  opphllem6  24244  lnopp2hpgb  24252  hpgerlem  24254  lmieu  24270  f1otrg  24295  f1otrge  24296  axeuclidlem  24386  axcontlem2  24389  usgraidx2vlem2  24513  usgrares1  24531  nbgraf1olem5  24566  usgra2wlkspth  24742  constr3cycl  24782  clwlkisclwwlklem1  24908  wwlkext2clwwlk  24924  eupath2  25101  frisusgranb  25118  frgra2v  25120  frgra3vlem2  25122  2pthfrgrarn2  25131  2spotiundisj  25183  usg2spot2nb  25186  usgreghash2spotv  25187  numclwwlk2lem1  25223  isgrp2d  25354  ubthlem3  25905  chirredlem1  27425  chirredlem3  27427  cdj1i  27468  xrge0infss  27730  omndmul2  27855  submarchi  27883  gsumle  27923  xrge0tsmsd  27929  suborng  27959  isarchiofld  27961  fimaproj  27990  locfinreflem  27997  cmppcmp  28015  ordtrest2NEWlem  28058  ordtconlem1  28060  lmdvg  28089  esumpcvgval  28226  esum2d  28241  sigapildsys  28307  volmeas  28359  imambfm  28389  omssubadd  28427  carsggect  28445  carsgclctunlem3  28447  sgnmul  28664  signsply0  28691  signstres  28715  lgamucov  28769  erdszelem8  28831  pconcon  28865  cvmlift2lem12  28948  cvmlift3lem5  28957  cvmlift3lem7  28959  cvmlift3lem8  28960  mrsubrn  29062  msrval  29087  msubff1  29105  nodenselem5  29610  btwnconn1lem13  29902  ltflcei  30208  heicant  30214  mblfinlem2  30217  mblfinlem3  30218  mblfinlem4  30219  cnambfre  30228  itg2addnclem  30232  itg2addnclem2  30233  itg2gt0cn  30236  bddiblnc  30251  ftc1cnnc  30255  ftc1anclem5  30260  ftc1anclem7  30262  ftc1anc  30264  elicc3  30301  neibastop2lem  30344  equivtotbnd  30440  isbndx  30444  ssbnd  30450  heibor1lem  30471  rrncmslem  30494  elrfi  30792  eldioph2  30860  diophin  30871  irrapxlem2  30924  irrapxlem3  30925  irrapxlem4  30926  irrapxlem5  30927  pell1234qrne0  30954  pell1234qrreccl  30955  pell1234qrmulcl  30956  pell14qrgt0  30960  pell14qrdich  30970  pell1qrge1  30971  pellfundex  30987  congabseq  31077  jm2.27b  31114  jm2.27  31116  fnwe2lem2  31163  kelac1  31175  lnrfg  31236  hbt  31247  cntzsdrg  31319  cvgdvgrat  31362  lcmgcdlem  31380  binomcxplemnotnn0  31429  mccl  31772  limcrecl  31801  lptioo2  31803  lptioo1  31804  lptre2pt  31812  addlimc  31820  icccncfext  31856  cncfiooicclem1  31862  cncfiooiccre  31864  dvbdfbdioolem2  31892  ioodvbdlimc1lem1  31894  dvnxpaek  31905  dvmptfprodlem  31907  dvmptfprod  31908  dvnprodlem3  31911  itgioocnicc  31942  itgspltprt  31944  stoweidlem31  31979  fourierdlem39  32094  fourierdlem42  32097  fourierdlem48  32103  fourierdlem49  32104  fourierdlem50  32105  fourierdlem51  32106  fourierdlem64  32119  fourierdlem65  32120  fourierdlem74  32129  fourierdlem75  32130  fourierdlem81  32136  fourierdlem82  32137  fourierdlem101  32156  etransclem23  32206  etransclem27  32210  etransclem32  32215  etransclem33  32216  etransclem35  32218  etransclem38  32221  proththd  32548  usgra2pthspth  32669  usgvad2edg  32729  resmgmhm2b  32806  2zrngmmgm  32952  cznrng  32963  rnghmsubcsetclem2  32984  rhmsubcsetclem2  33030  srhmsubc  33084  rhmsubclem4  33097  srhmsubcALTV  33103  rhmsubcALTVlem4  33116  lincsum  33230  lcoss  33237  snlindsntor  33272  islindeps2  33284  ad5ant12  33565  sineq0ALT  34084  islshpat  35155  lfl1dim  35259  lfl1dim2N  35260  lkrpssN  35301  glbconN  35514  hlhgt2  35526  3dim2  35605  3dim3  35606  islln3  35647  islvol5  35716  2lplnja  35756  dalem19  35819  isline4N  35914  2polssN  36052  lhpmatb  36168  4atex  36213  trlatn0  36310  cdlemf2  36701  dialss  37186  diaglbN  37195  diaintclN  37198  dibglbN  37306  dibintclN  37307  dihlsscpre  37374  dihglblem5aN  37432  dihglblem2aN  37433  dihglblem4  37437  dihatexv  37478  dihjat1lem  37568  lcfl6  37640  mapdval2N  37770
  Copyright terms: Public domain W3C validator