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

Theorem ad3antrrr 712
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 453 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 708 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ad4antr  714  oaabs  6888  oaabs2  6889  omabs  6891  undom  7197  sbthlem8  7225  findcard3  7351  cantnfle  7627  cantnfp1  7638  cantnflem1c  7644  sornom  8158  enfin2i  8202  ttukeylem6  8395  fpwwe2lem13  8518  fpwwe2  8519  winalim2  8572  wuncval2  8623  xlemul1a  10868  difreicc  11029  faclbnd  11582  ello12  12311  lo1bdd2  12319  elo12  12322  rlimclim1  12340  rlimcld2  12373  o1co  12381  o1of2  12407  o1rlimmul  12413  rlimsqzlem  12443  isercoll  12462  o1fsum  12593  supcvg  12636  dvds2ln  12881  isprm5  13113  pcadd  13259  vdwlem2  13351  vdwlem11  13360  prdsval  13679  mreexexlem4d  13873  isacs2  13879  catcocl  13911  catass  13912  subccocl  14043  fullsubc  14048  funcco  14069  funcpropd  14098  fullpropd  14118  ffthiso  14127  isnat  14145  natpropd  14174  fucpropd  14175  xpcval  14275  evlf2  14316  curfpropd  14331  curfuncf  14336  uncfcurf  14337  curf2ndf  14345  hofcl  14357  hofpropd  14365  yonffthlem  14380  isacs3lem  14593  acsfiindd  14604  resmhm2b  14762  conjnmzb  15041  pgpfi  15240  sylow3lem2  15263  efgredlem  15380  frgpnabllem1  15485  dprdfcntz  15574  ablfac1b  15629  pgpfac1lem3  15636  pgpfac1lem5  15638  pgpfaclem3  15642  islmhm2  16115  lspsneleq  16188  psrval  16430  psrass1  16470  resspsrmul  16481  mplbas2  16532  coe1tmmul  16670  znunit  16845  neiptoptop  17196  neitr  17245  ordtrest2lem  17268  cnpnei  17329  iscncl  17334  cncls  17339  cnntr  17340  cncnp  17345  lmcnp  17369  isreg2  17442  hauscmplem  17470  cmpfi  17472  1stcfb  17509  1stcrest  17517  2ndcctbss  17519  2ndcomap  17522  islly2  17548  cldllycmp  17559  lly1stc  17560  llycmpkgen2  17583  1stckgenlem  17586  kgencn2  17590  kgencn3  17591  ptbasfi  17614  ptpjopn  17645  txdis1cn  17668  txlly  17669  txnlly  17670  txtube  17673  txcmplem2  17675  tx1stc  17683  txkgen  17685  xkopt  17688  xkoco2cn  17691  xkococnlem  17692  xkococn  17693  xkoinjcn  17720  tgqtop  17745  regr1lem  17772  kqreglem1  17774  nrmhmph  17827  rnelfmlem  17985  rnelfm  17986  fmfnfmlem4  17990  fmfnfm  17991  ufldom  17995  flimopn  18008  hauspwpwf1  18020  fclsopn  18047  fclsnei  18052  fclsrest  18057  alexsublem  18076  alexsubALTlem3  18081  ptcmplem2  18085  ptcmplem3  18086  cnextfun  18096  cnextcn  18099  symgtgp  18132  tgpt0  18149  divstgpopn  18150  tsmsxplem1  18183  trust  18260  utopsnneiplem  18278  utop3cls  18282  utopreg  18283  isucn2  18310  cstucnd  18315  ucncn  18316  fmucnd  18323  cfilufg  18324  neipcfilu  18327  met2ndci  18553  prdsxmslem2  18560  metcnp3  18571  metustidOLD  18590  metustid  18591  metustexhalfOLD  18594  metustexhalf  18595  metustOLD  18598  metust  18599  metutopOLD  18613  psmetutop  18614  nmoleub  18766  reconnlem2  18859  xrge0tsms  18866  cncfco  18938  lebnumlem3  18989  lebnum  18990  nmoleub2lem2  19125  nmoleub3  19128  iscfil2  19220  iscau4  19233  iscmet3lem2  19246  equivcfil  19253  equivcau  19254  caubl  19261  ovolshftlem2  19407  ovolicc2lem4  19417  uniioombl  19482  i1fmulclem  19595  mbfi1fseqlem6  19613  itg2const2  19634  itg2split  19642  ellimc2  19765  ellimc3  19767  limcflf  19769  dvmptfsum  19860  dvferm1  19870  dvferm2  19872  dvlip2  19880  c1lip1  19882  lhop1  19899  ftc1a  19922  ply1divex  20060  plyeq0lem  20130  plymullem1  20134  coemullem  20169  coemulc  20174  ulmshftlem  20306  ulmcaulem  20311  ulmbdd  20315  ulmcn  20316  ulmdvlem3  20319  mtestbdd  20322  pserulm  20339  pserdvlem2  20345  abelthlem8  20356  xrlimcnp  20808  jensen  20828  logfac2  21002  dchrelbas3  21023  dchrpt  21052  lgsquad3  21146  2sqb  21163  rpvmasumlem  21182  dchrisumlem1  21184  dchrisumlem3  21186  dchrmusum2  21189  dchrvmasumlem2  21193  dchrisum0flblem1  21203  dchrisum0lem1b  21210  dchrisum0lem1  21211  dchrisum0  21215  mulog2sumlem2  21230  pntlem3  21304  ostth3  21333  usgraidx2vlem2  21412  usgrares1  21425  nbgraf1olem5  21456  constr3cycl  21649  eupath2  21703  isgrp2d  21824  ubthlem3  22375  chirredlem1  23894  chirredlem3  23896  cdj1i  23937  gsumpropd2lem  24221  xrge0tsmsd  24224  subofld  24246  lmdvg  24339  esumpcvgval  24469  volmeas  24588  imambfm  24613  lgamucov  24823  erdszelem8  24885  pconcon  24919  cvmlift2lem12  25002  cvmlift3lem5  25011  cvmlift3lem7  25013  cvmlift3lem8  25014  nodenselem5  25641  axeuclidlem  25902  axcontlem2  25905  btwnconn1lem13  26034  ltflcei  26240  lxflflp1  26242  mblfinlem2  26245  mblfinlem3  26246  mblfinlem4  26247  cnambfre  26256  itg2addnclem  26257  itg2addnclem2  26258  itg2gt0cn  26261  bddiblnc  26276  ftc1cnnc  26280  ftc1anclem5  26285  ftc1anclem7  26287  ftc1anc  26289  elicc3  26321  locfincmp  26385  neibastop2lem  26390  sstotbnd2  26484  equivtotbnd  26488  isbndx  26492  ssbnd  26498  heibor1lem  26519  rrncmslem  26542  elrfi  26749  eldioph2  26821  diophin  26832  irrapxlem2  26887  irrapxlem3  26888  irrapxlem4  26889  irrapxlem5  26890  pell1234qrne0  26917  pell1234qrreccl  26918  pell1234qrmulcl  26919  pell14qrgt0  26923  pell1234qrdich  26925  pell14qrdich  26933  pell1qrge1  26934  pellfundex  26950  congabseq  27040  jm2.27b  27078  jm2.27  27080  fnwe2lem2  27127  kelac1  27139  uvcff  27218  uvcf1  27219  lindfmm  27275  lnrfg  27301  hbt  27312  cntzsdrg  27488  stoweidlem31  27757  swrdswrd  28200  swrdccatin12lem4  28214  swrdccat3blem  28219  usgra2pthspth  28306  usgra2wlkspth  28309  frisusgranb  28388  frgra3vlem2  28392  2pthfrgrarn2  28401  usg2spot2nb  28455  usgreghash2spotv  28456  ad5ant12  28547  sineq0ALT  29050  islshpat  29816  lfl1dim  29920  lfl1dim2N  29921  lkrpssN  29962  glbconN  30175  hlhgt2  30187  3dim2  30266  3dim3  30267  islln3  30308  islvol5  30377  2lplnja  30417  dalem19  30480  isline4N  30575  2polssN  30713  lhpmatb  30829  4atex  30874  trlatn0  30970  cdlemf2  31360  dialss  31845  diaglbN  31854  diaintclN  31857  dibglbN  31965  dibintclN  31966  dihlsscpre  32033  dihglblem5aN  32091  dihglblem2aN  32092  dihglblem4  32096  dihatexv  32137  dihjat1lem  32227  lcfl6  32299  mapdval2N  32429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator