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  6889  oaabs2  6890  omabs  6892  undom  7198  sbthlem8  7226  findcard3  7352  cantnfle  7628  cantnfp1  7639  cantnflem1c  7645  sornom  8159  enfin2i  8203  ttukeylem6  8396  fpwwe2lem13  8519  fpwwe2  8520  winalim2  8573  wuncval2  8624  xlemul1a  10869  difreicc  11030  faclbnd  11583  ello12  12312  lo1bdd2  12320  elo12  12323  rlimclim1  12341  rlimcld2  12374  o1co  12382  o1of2  12408  o1rlimmul  12414  rlimsqzlem  12444  isercoll  12463  o1fsum  12594  supcvg  12637  dvds2ln  12882  isprm5  13114  pcadd  13260  vdwlem2  13352  vdwlem11  13361  prdsval  13680  mreexexlem4d  13874  isacs2  13880  catcocl  13912  catass  13913  subccocl  14044  fullsubc  14049  funcco  14070  funcpropd  14099  fullpropd  14119  ffthiso  14128  isnat  14146  natpropd  14175  fucpropd  14176  xpcval  14276  evlf2  14317  curfpropd  14332  curfuncf  14337  uncfcurf  14338  curf2ndf  14346  hofcl  14358  hofpropd  14366  yonffthlem  14381  isacs3lem  14594  acsfiindd  14605  resmhm2b  14763  conjnmzb  15042  pgpfi  15241  sylow3lem2  15264  efgredlem  15381  frgpnabllem1  15486  dprdfcntz  15575  ablfac1b  15630  pgpfac1lem3  15637  pgpfac1lem5  15639  pgpfaclem3  15643  islmhm2  16116  lspsneleq  16189  psrval  16431  psrass1  16471  resspsrmul  16482  mplbas2  16533  coe1tmmul  16671  znunit  16846  neiptoptop  17197  neitr  17246  ordtrest2lem  17269  cnpnei  17330  iscncl  17335  cncls  17340  cnntr  17341  cncnp  17346  lmcnp  17370  isreg2  17443  hauscmplem  17471  cmpfi  17473  1stcfb  17510  1stcrest  17518  2ndcctbss  17520  2ndcomap  17523  islly2  17549  cldllycmp  17560  lly1stc  17561  llycmpkgen2  17584  1stckgenlem  17587  kgencn2  17591  kgencn3  17592  ptbasfi  17615  ptpjopn  17646  txdis1cn  17669  txlly  17670  txnlly  17671  txtube  17674  txcmplem2  17676  tx1stc  17684  txkgen  17686  xkopt  17689  xkoco2cn  17692  xkococnlem  17693  xkococn  17694  xkoinjcn  17721  tgqtop  17746  regr1lem  17773  kqreglem1  17775  nrmhmph  17828  rnelfmlem  17986  rnelfm  17987  fmfnfmlem4  17991  fmfnfm  17992  ufldom  17996  flimopn  18009  hauspwpwf1  18021  fclsopn  18048  fclsnei  18053  fclsrest  18058  alexsublem  18077  alexsubALTlem3  18082  ptcmplem2  18086  ptcmplem3  18087  cnextfun  18097  cnextcn  18100  symgtgp  18133  tgpt0  18150  divstgpopn  18151  tsmsxplem1  18184  trust  18261  utopsnneiplem  18279  utop3cls  18283  utopreg  18284  isucn2  18311  cstucnd  18316  ucncn  18317  fmucnd  18324  cfilufg  18325  neipcfilu  18328  met2ndci  18554  prdsxmslem2  18561  metcnp3  18572  metustidOLD  18591  metustid  18592  metustexhalfOLD  18595  metustexhalf  18596  metustOLD  18599  metust  18600  metutopOLD  18614  psmetutop  18615  nmoleub  18767  reconnlem2  18860  xrge0tsms  18867  cncfco  18939  lebnumlem3  18990  lebnum  18991  nmoleub2lem2  19126  nmoleub3  19129  iscfil2  19221  iscau4  19234  iscmet3lem2  19247  equivcfil  19254  equivcau  19255  caubl  19262  ovolshftlem2  19408  ovolicc2lem4  19418  uniioombl  19483  i1fmulclem  19596  mbfi1fseqlem6  19614  itg2const2  19635  itg2split  19643  ellimc2  19766  ellimc3  19768  limcflf  19770  dvmptfsum  19861  dvferm1  19871  dvferm2  19873  dvlip2  19881  c1lip1  19883  lhop1  19900  ftc1a  19923  ply1divex  20061  plyeq0lem  20131  plymullem1  20135  coemullem  20170  coemulc  20175  ulmshftlem  20307  ulmcaulem  20312  ulmbdd  20316  ulmcn  20317  ulmdvlem3  20320  mtestbdd  20323  pserulm  20340  pserdvlem2  20346  abelthlem8  20357  xrlimcnp  20809  jensen  20829  logfac2  21003  dchrelbas3  21024  dchrpt  21053  lgsquad3  21147  2sqb  21164  rpvmasumlem  21183  dchrisumlem1  21185  dchrisumlem3  21187  dchrmusum2  21190  dchrvmasumlem2  21194  dchrisum0flblem1  21204  dchrisum0lem1b  21211  dchrisum0lem1  21212  dchrisum0  21216  mulog2sumlem2  21231  pntlem3  21305  ostth3  21334  usgraidx2vlem2  21413  usgrares1  21426  nbgraf1olem5  21457  constr3cycl  21650  eupath2  21704  isgrp2d  21825  ubthlem3  22376  chirredlem1  23895  chirredlem3  23897  cdj1i  23938  gsumpropd2lem  24222  xrge0tsmsd  24225  subofld  24247  lmdvg  24340  esumpcvgval  24470  volmeas  24589  imambfm  24614  lgamucov  24824  erdszelem8  24886  pconcon  24920  cvmlift2lem12  25003  cvmlift3lem5  25012  cvmlift3lem7  25014  cvmlift3lem8  25015  nodenselem5  25642  axeuclidlem  25903  axcontlem2  25906  btwnconn1lem13  26035  ltflcei  26241  lxflflp1  26243  mblfinlem2  26246  mblfinlem3  26247  mblfinlem4  26248  cnambfre  26257  itg2addnclem  26258  itg2addnclem2  26259  itg2gt0cn  26262  bddiblnc  26277  ftc1cnnc  26281  ftc1anclem5  26286  ftc1anclem7  26288  ftc1anc  26290  elicc3  26322  locfincmp  26386  neibastop2lem  26391  sstotbnd2  26485  equivtotbnd  26489  isbndx  26493  ssbnd  26499  heibor1lem  26520  rrncmslem  26543  elrfi  26750  eldioph2  26822  diophin  26833  irrapxlem2  26888  irrapxlem3  26889  irrapxlem4  26890  irrapxlem5  26891  pell1234qrne0  26918  pell1234qrreccl  26919  pell1234qrmulcl  26920  pell14qrgt0  26924  pell1234qrdich  26926  pell14qrdich  26934  pell1qrge1  26935  pellfundex  26951  congabseq  27041  jm2.27b  27079  jm2.27  27081  fnwe2lem2  27128  kelac1  27140  uvcff  27219  uvcf1  27220  lindfmm  27276  lnrfg  27302  hbt  27313  cntzsdrg  27489  stoweidlem31  27758  swrdswrd  28221  swrdccatin12lem4  28235  swrdccat3blem  28240  usgra2pthspth  28331  usgra2wlkspth  28334  frisusgranb  28449  frgra3vlem2  28453  2pthfrgrarn2  28462  usg2spot2nb  28516  usgreghash2spotv  28517  ad5ant12  28608  sineq0ALT  29111  islshpat  29877  lfl1dim  29981  lfl1dim2N  29982  lkrpssN  30023  glbconN  30236  hlhgt2  30248  3dim2  30327  3dim3  30328  islln3  30369  islvol5  30438  2lplnja  30478  dalem19  30541  isline4N  30636  2polssN  30774  lhpmatb  30890  4atex  30935  trlatn0  31031  cdlemf2  31421  dialss  31906  diaglbN  31915  diaintclN  31918  dibglbN  32026  dibintclN  32027  dihlsscpre  32094  dihglblem5aN  32152  dihglblem2aN  32153  dihglblem4  32157  dihatexv  32198  dihjat1lem  32288  lcfl6  32360  mapdval2N  32490
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