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

Theorem ad3antrrr 711
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 452 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 707 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad4antr  713  oaabs  6846  oaabs2  6847  omabs  6849  undom  7155  sbthlem8  7183  findcard3  7309  cantnfle  7582  cantnfp1  7593  cantnflem1c  7599  sornom  8113  enfin2i  8157  ttukeylem6  8350  fpwwe2lem13  8473  fpwwe2  8474  winalim2  8527  wuncval2  8578  xlemul1a  10823  difreicc  10984  faclbnd  11536  ello12  12265  lo1bdd2  12273  elo12  12276  rlimclim1  12294  rlimcld2  12327  o1co  12335  o1of2  12361  o1rlimmul  12367  rlimsqzlem  12397  isercoll  12416  o1fsum  12547  supcvg  12590  dvds2ln  12835  isprm5  13067  pcadd  13213  vdwlem2  13305  vdwlem11  13314  prdsval  13633  mreexexlem4d  13827  isacs2  13833  catcocl  13865  catass  13866  subccocl  13997  fullsubc  14002  funcco  14023  funcpropd  14052  fullpropd  14072  ffthiso  14081  isnat  14099  natpropd  14128  fucpropd  14129  xpcval  14229  evlf2  14270  curfpropd  14285  curfuncf  14290  uncfcurf  14291  curf2ndf  14299  hofcl  14311  hofpropd  14319  yonffthlem  14334  isacs3lem  14547  acsfiindd  14558  resmhm2b  14716  conjnmzb  14995  pgpfi  15194  sylow3lem2  15217  efgredlem  15334  frgpnabllem1  15439  dprdfcntz  15528  ablfac1b  15583  pgpfac1lem3  15590  pgpfac1lem5  15592  pgpfaclem3  15596  islmhm2  16069  lspsneleq  16142  psrval  16384  psrass1  16424  resspsrmul  16435  mplbas2  16486  coe1tmmul  16624  znunit  16799  neiptoptop  17150  neitr  17198  ordtrest2lem  17221  cnpnei  17282  iscncl  17287  cncls  17292  cnntr  17293  cncnp  17298  lmcnp  17322  isreg2  17395  hauscmplem  17423  cmpfi  17425  1stcfb  17461  1stcrest  17469  2ndcctbss  17471  2ndcomap  17474  islly2  17500  cldllycmp  17511  lly1stc  17512  llycmpkgen2  17535  1stckgenlem  17538  kgencn2  17542  kgencn3  17543  ptbasfi  17566  ptpjopn  17597  txdis1cn  17620  txlly  17621  txnlly  17622  txtube  17625  txcmplem2  17627  tx1stc  17635  txkgen  17637  xkopt  17640  xkoco2cn  17643  xkococnlem  17644  xkococn  17645  xkoinjcn  17672  tgqtop  17697  regr1lem  17724  kqreglem1  17726  nrmhmph  17779  rnelfmlem  17937  rnelfm  17938  fmfnfmlem4  17942  fmfnfm  17943  ufldom  17947  flimopn  17960  hauspwpwf1  17972  fclsopn  17999  fclsnei  18004  fclsrest  18009  alexsublem  18028  alexsubALTlem3  18033  ptcmplem2  18037  ptcmplem3  18038  cnextfun  18048  cnextcn  18051  symgtgp  18084  tgpt0  18101  divstgpopn  18102  tsmsxplem1  18135  trust  18212  utopsnneiplem  18230  utop3cls  18234  utopreg  18235  isucn2  18262  cstucnd  18267  ucncn  18268  fmucnd  18275  cfilufg  18276  neipcfilu  18279  met2ndci  18505  prdsxmslem2  18512  metcnp3  18523  metustidOLD  18542  metustid  18543  metustexhalfOLD  18546  metustexhalf  18547  metustOLD  18550  metust  18551  metutopOLD  18565  psmetutop  18566  nmoleub  18718  reconnlem2  18811  xrge0tsms  18818  cncfco  18890  lebnumlem3  18941  lebnum  18942  nmoleub2lem2  19077  nmoleub3  19080  iscfil2  19172  iscau4  19185  iscmet3lem2  19198  equivcfil  19205  equivcau  19206  caubl  19213  ovolshftlem2  19359  ovolicc2lem4  19369  uniioombl  19434  i1fmulclem  19547  mbfi1fseqlem6  19565  itg2const2  19586  itg2split  19594  ellimc2  19717  ellimc3  19719  limcflf  19721  dvmptfsum  19812  dvferm1  19822  dvferm2  19824  dvlip2  19832  c1lip1  19834  lhop1  19851  ftc1a  19874  ply1divex  20012  plyeq0lem  20082  plymullem1  20086  coemullem  20121  coemulc  20126  ulmshftlem  20258  ulmcaulem  20263  ulmbdd  20267  ulmcn  20268  ulmdvlem3  20271  mtestbdd  20274  pserulm  20291  pserdvlem2  20297  abelthlem8  20308  xrlimcnp  20760  jensen  20780  logfac2  20954  dchrelbas3  20975  dchrpt  21004  lgsquad3  21098  2sqb  21115  rpvmasumlem  21134  dchrisumlem1  21136  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasumlem2  21145  dchrisum0flblem1  21155  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0  21167  mulog2sumlem2  21182  pntlem3  21256  ostth3  21285  usgraidx2vlem2  21364  usgrares1  21377  nbgraf1olem5  21408  constr3cycl  21601  eupath2  21655  isgrp2d  21776  ubthlem3  22327  chirredlem1  23846  chirredlem3  23848  cdj1i  23889  gsumpropd2lem  24173  xrge0tsmsd  24176  subofld  24198  lmdvg  24291  esumpcvgval  24421  volmeas  24540  imambfm  24565  lgamucov  24775  erdszelem8  24837  pconcon  24871  cvmlift2lem12  24954  cvmlift3lem5  24963  cvmlift3lem7  24965  cvmlift3lem8  24966  nodenselem5  25553  axeuclidlem  25805  axcontlem2  25808  btwnconn1lem13  25937  ltflcei  26140  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  itg2gt0cn  26159  bddiblnc  26174  ftc1cnnc  26178  elicc3  26210  locfincmp  26274  neibastop2lem  26279  sstotbnd2  26373  equivtotbnd  26377  isbndx  26381  ssbnd  26387  heibor1lem  26408  rrncmslem  26431  elrfi  26638  eldioph2  26710  diophin  26721  irrapxlem2  26776  irrapxlem3  26777  irrapxlem4  26778  irrapxlem5  26779  pell1234qrne0  26806  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell14qrgt0  26812  pell1234qrdich  26814  pell14qrdich  26822  pell1qrge1  26823  pellfundex  26839  congabseq  26929  jm2.27b  26967  jm2.27  26969  fnwe2lem2  27016  kelac1  27029  uvcff  27108  uvcf1  27109  lindfmm  27165  lnrfg  27191  hbt  27202  cntzsdrg  27378  stoweidlem31  27647  swrdswrd  28011  usgra2pthspth  28035  usgra2wlkspth  28038  frisusgranb  28101  frgra3vlem2  28105  2pthfrgrarn2  28114  usg2spot2nb  28168  usgreghash2spotv  28169  ad5ant12  28260  islshpat  29500  lfl1dim  29604  lfl1dim2N  29605  lkrpssN  29646  glbconN  29859  hlhgt2  29871  3dim2  29950  3dim3  29951  islln3  29992  islvol5  30061  2lplnja  30101  dalem19  30164  isline4N  30259  2polssN  30397  lhpmatb  30513  4atex  30558  trlatn0  30654  cdlemf2  31044  dialss  31529  diaglbN  31538  diaintclN  31541  dibglbN  31649  dibintclN  31650  dihlsscpre  31717  dihglblem5aN  31775  dihglblem2aN  31776  dihglblem4  31780  dihatexv  31821  dihjat1lem  31911  lcfl6  31983  mapdval2N  32113
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 178  df-an 361
  Copyright terms: Public domain W3C validator