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  7290  oaabs2  7291  omabs  7293  undom  7602  sbthlem8  7631  findcard3  7759  cantnfle  8086  cantnfp1  8096  cantnflem1c  8102  cantnfleOLD  8116  cantnfp1OLD  8122  cantnflem1cOLD  8125  sornom  8653  enfin2i  8697  ttukeylem6  8890  fpwwe2lem13  9016  fpwwe2  9017  winalim2  9070  wuncval2  9121  xlemul1a  11476  difreicc  11648  faclbnd  12330  swrdswrd  12642  swrdccatin12lem3  12672  swrdccat3blem  12677  ello12  13295  lo1bdd2  13303  elo12  13306  rlimclim1  13324  rlimcld2  13357  o1co  13365  o1of2  13391  o1rlimmul  13397  rlimsqzlem  13427  isercoll  13446  o1fsum  13583  supcvg  13623  dvds2ln  13868  isprm5  14105  pcadd  14260  vdwlem2  14352  vdwlem11  14361  sbcie3s  14527  prdsval  14703  mreexexlem4d  14895  isacs2  14901  catcocl  14933  catass  14934  subccocl  15065  fullsubc  15070  funcco  15091  funcpropd  15120  fullpropd  15140  ffthiso  15149  isnat  15167  natpropd  15196  fucpropd  15197  xpcval  15297  evlf2  15338  curfpropd  15353  curfuncf  15358  uncfcurf  15359  curf2ndf  15367  hofcl  15379  hofpropd  15387  yonffthlem  15402  isacs3lem  15646  acsfiindd  15657  resmhm2b  15799  gsumpropd2lem  15815  conjnmzb  16093  pgpfi  16418  sylow3lem2  16441  efgredlem  16558  frgpnabllem1  16665  dprdfcntz  16836  dprdfcntzOLD  16842  ablfac1b  16908  pgpfac1lem3  16915  pgpfac1lem5  16917  pgpfaclem3  16921  islmhm2  17464  lspsneleq  17541  psrval  17779  psrass1  17828  resspsrmul  17840  mplbas2  17902  mplbas2OLD  17903  coe1tmmul  18086  gsummoncoe1  18114  znunit  18366  psgndiflemB  18400  uvcff  18586  uvcf1  18587  lindfmm  18626  dmatsubcl  18764  scmatscm  18779  smatvscl  18790  marrepval  18828  mdetdiaglem  18864  mdetunilem8  18885  mdetunilem9  18886  pmatcoe1fsupp  18966  decpmatmulsumfsupp  19038  pmatcollpw2lem  19042  mp2pm2mplem4  19074  pm2mpmhmlem1  19083  pm2mpmhmlem2  19084  pm2mp  19090  fvmptnn04if  19114  cpmadugsumfi  19142  cpmidg2sum  19145  cpmadumatpoly  19148  cayhamlem4  19153  neiptoptop  19395  neitr  19444  ordtrest2lem  19467  cnpnei  19528  iscncl  19533  cncls  19538  cnntr  19539  cncnp  19544  lmcnp  19568  isreg2  19641  hauscmplem  19669  cmpfi  19671  1stcfb  19709  1stcrest  19717  2ndcctbss  19719  2ndcomap  19722  islly2  19748  cldllycmp  19759  lly1stc  19760  llycmpkgen2  19783  1stckgenlem  19786  kgencn2  19790  kgencn3  19791  ptbasfi  19814  ptpjopn  19845  txdis1cn  19868  txlly  19869  txnlly  19870  txtube  19873  txcmplem2  19875  tx1stc  19883  txkgen  19885  xkopt  19888  xkoco2cn  19891  xkococnlem  19892  xkococn  19893  xkoinjcn  19920  tgqtop  19945  regr1lem  19972  kqreglem1  19974  nrmhmph  20027  rnelfmlem  20185  rnelfm  20186  fmfnfmlem4  20190  fmfnfm  20191  ufldom  20195  flimopn  20208  hauspwpwf1  20220  fclsopn  20247  fclsnei  20252  fclsrest  20257  alexsublem  20276  alexsubALTlem3  20281  ptcmplem2  20285  ptcmplem3  20286  cnextfun  20296  cnextcn  20299  symgtgp  20332  tgpt0  20349  divstgpopn  20350  tsmsxplem1  20387  trust  20464  utopsnneiplem  20482  utop3cls  20486  utopreg  20487  isucn2  20514  cstucnd  20519  ucncn  20520  fmucnd  20527  cfilufg  20528  neipcfilu  20531  met2ndci  20757  prdsxmslem2  20764  metcnp3  20775  metustidOLD  20794  metustid  20795  metustexhalfOLD  20798  metustexhalf  20799  metustOLD  20802  metust  20803  metutopOLD  20817  psmetutop  20818  nmoleub  20970  reconnlem2  21064  xrge0tsms  21071  cncfco  21143  lebnumlem3  21195  lebnum  21196  nmoleub2lem2  21331  nmoleub3  21334  iscfil2  21437  iscau4  21450  iscmet3lem2  21463  equivcfil  21470  equivcau  21471  caubl  21478  rrxdstprj1  21568  ovolshftlem2  21653  ovolicc2lem4  21663  uniioombl  21730  i1fmulclem  21841  mbfi1fseqlem6  21859  itg2const2  21880  itg2split  21888  ellimc2  22013  ellimc3  22015  limcflf  22017  dvmptfsum  22108  dvferm1  22118  dvferm2  22120  dvlip2  22128  c1lip1  22130  lhop1  22147  ftc1a  22170  ply1divex  22269  plyeq0lem  22339  plymullem1  22343  coemullem  22378  coemulc  22383  ulmshftlem  22515  ulmcaulem  22520  ulmbdd  22524  ulmcn  22525  ulmdvlem3  22528  mtestbdd  22531  pserulm  22548  pserdvlem2  22554  abelthlem8  22565  xrlimcnp  23023  jensen  23043  logfac2  23217  dchrelbas3  23238  dchrpt  23267  lgsquad3  23361  2sqb  23378  rpvmasumlem  23397  dchrisumlem1  23399  dchrisumlem3  23401  dchrmusum2  23404  dchrvmasumlem2  23408  dchrisum0flblem1  23418  dchrisum0lem1b  23425  dchrisum0lem1  23426  dchrisum0  23430  mulog2sumlem2  23445  pntlem3  23519  ostth3  23548  istrkgcb  23578  tgbtwndiff  23622  tgcgrxfr  23634  motcgrg  23656  lnext  23678  tgbtwnconn1  23686  tgbtwnconn3  23688  legval  23695  legtrid  23702  legso  23709  tglnne  23719  tglineeltr  23722  colline  23740  tglowdim2l  23741  tglowdim2ln  23742  mirreu3  23745  krippenlem  23772  midexlem  23774  perpcom  23795  perpneq  23796  footex  23800  colperpexlem3  23808  colperpex  23809  mideulem  23810  mideu  23811  lmieu  23824  f1otrg  23847  f1otrge  23848  axeuclidlem  23938  axcontlem2  23941  usgraidx2vlem2  24065  usgrares1  24083  nbgraf1olem5  24118  usgra2wlkspth  24294  constr3cycl  24334  clwlkisclwwlklem1  24460  wwlkext2clwwlk  24476  eupath2  24653  frisusgranb  24670  frgra2v  24672  frgra3vlem2  24674  2pthfrgrarn2  24683  usg2spot2nb  24739  usgreghash2spotv  24740  numclwwlk2lem1  24776  isgrp2d  24910  ubthlem3  25461  chirredlem1  26982  chirredlem3  26984  cdj1i  27025  xrge0infss  27245  omndmul2  27361  submarchi  27389  gsumle  27430  xrge0tsmsd  27435  suborng  27465  isarchiofld  27467  fimaproj  27496  ordtrest2NEWlem  27537  ordtconlem1  27539  lmdvg  27568  qtophaus  27634  esumpcvgval  27721  volmeas  27840  imambfm  27870  sgnmul  28118  signsply0  28145  signstres  28169  lgamucov  28217  erdszelem8  28279  pconcon  28313  cvmlift2lem12  28396  cvmlift3lem5  28405  cvmlift3lem7  28407  cvmlift3lem8  28408  nodenselem5  29019  btwnconn1lem13  29323  ltflcei  29617  lxflflp1  29619  heicant  29624  mblfinlem2  29627  mblfinlem3  29628  mblfinlem4  29629  cnambfre  29638  itg2addnclem  29641  itg2addnclem2  29642  itg2gt0cn  29645  bddiblnc  29660  ftc1cnnc  29664  ftc1anclem5  29669  ftc1anclem7  29671  ftc1anc  29673  elicc3  29710  locfincmp  29774  neibastop2lem  29779  sstotbnd2  29871  equivtotbnd  29875  isbndx  29879  ssbnd  29885  heibor1lem  29906  rrncmslem  29929  elrfi  30228  eldioph2  30297  diophin  30308  irrapxlem2  30361  irrapxlem3  30362  irrapxlem4  30363  irrapxlem5  30364  pell1234qrne0  30391  pell1234qrreccl  30392  pell1234qrmulcl  30393  pell14qrgt0  30397  pell1234qrdich  30399  pell14qrdich  30407  pell1qrge1  30408  pellfundex  30424  congabseq  30514  jm2.27b  30552  jm2.27  30554  fnwe2lem2  30601  kelac1  30613  lnrfg  30672  hbt  30683  cntzsdrg  30756  lcmgcdlem  30812  limcrecl  31171  lptioo2  31173  lptioo1  31174  lptre2pt  31182  icccncfext  31226  cncfiooicclem1  31232  cncfiooiccre  31234  fperdvper  31248  ioodvbdlimc1lem1  31261  itgioocnicc  31295  itgspltprt  31297  stoweidlem31  31331  fourierdlem39  31446  fourierdlem42  31449  fourierdlem45  31452  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem51  31458  fourierdlem64  31471  fourierdlem65  31472  fourierdlem74  31481  fourierdlem75  31482  fourierdlem81  31488  fourierdlem82  31489  fourierdlem87  31494  fourierdlem101  31508  usgra2pthspth  31820  usgvad2edg  31880  lincsum  32103  lcoss  32110  snlindsntor  32145  islindeps2  32157  ad5ant12  32311  sineq0ALT  32817  islshpat  33814  lfl1dim  33918  lfl1dim2N  33919  lkrpssN  33960  glbconN  34173  hlhgt2  34185  3dim2  34264  3dim3  34265  islln3  34306  islvol5  34375  2lplnja  34415  dalem19  34478  isline4N  34573  2polssN  34711  lhpmatb  34827  4atex  34872  trlatn0  34968  cdlemf2  35358  dialss  35843  diaglbN  35852  diaintclN  35855  dibglbN  35963  dibintclN  35964  dihlsscpre  36031  dihglblem5aN  36089  dihglblem2aN  36090  dihglblem4  36094  dihatexv  36135  dihjat1lem  36225  lcfl6  36297  mapdval2N  36427
  Copyright terms: Public domain W3C validator