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  7075  oaabs2  7076  omabs  7078  undom  7391  sbthlem8  7420  findcard3  7547  cantnfle  7871  cantnfp1  7881  cantnflem1c  7887  cantnfleOLD  7901  cantnfp1OLD  7907  cantnflem1cOLD  7910  sornom  8438  enfin2i  8482  ttukeylem6  8675  fpwwe2lem13  8801  fpwwe2  8802  winalim2  8855  wuncval2  8906  xlemul1a  11243  difreicc  11409  faclbnd  12058  swrdswrd  12346  swrdccatin12lem3  12373  swrdccat3blem  12378  ello12  12986  lo1bdd2  12994  elo12  12997  rlimclim1  13015  rlimcld2  13048  o1co  13056  o1of2  13082  o1rlimmul  13088  rlimsqzlem  13118  isercoll  13137  o1fsum  13268  supcvg  13310  dvds2ln  13555  isprm5  13790  pcadd  13943  vdwlem2  14035  vdwlem11  14044  sbcie3s  14210  prdsval  14385  mreexexlem4d  14577  isacs2  14583  catcocl  14615  catass  14616  subccocl  14747  fullsubc  14752  funcco  14773  funcpropd  14802  fullpropd  14822  ffthiso  14831  isnat  14849  natpropd  14878  fucpropd  14879  xpcval  14979  evlf2  15020  curfpropd  15035  curfuncf  15040  uncfcurf  15041  curf2ndf  15049  hofcl  15061  hofpropd  15069  yonffthlem  15084  isacs3lem  15328  acsfiindd  15339  resmhm2b  15480  gsumpropd2lem  15496  conjnmzb  15772  pgpfi  16095  sylow3lem2  16118  efgredlem  16235  frgpnabllem1  16342  dprdfcntz  16487  dprdfcntzOLD  16493  ablfac1b  16559  pgpfac1lem3  16566  pgpfac1lem5  16568  pgpfaclem3  16572  islmhm2  17096  lspsneleq  17173  psrval  17406  psrass1  17455  resspsrmul  17466  mplbas2  17526  mplbas2OLD  17527  coe1tmmul  17705  znunit  17971  psgndiflemB  18005  uvcff  18191  uvcf1  18192  lindfmm  18231  marrepval  18348  mdetunilem8  18400  mdetunilem9  18401  neiptoptop  18710  neitr  18759  ordtrest2lem  18782  cnpnei  18843  iscncl  18848  cncls  18853  cnntr  18854  cncnp  18859  lmcnp  18883  isreg2  18956  hauscmplem  18984  cmpfi  18986  1stcfb  19024  1stcrest  19032  2ndcctbss  19034  2ndcomap  19037  islly2  19063  cldllycmp  19074  lly1stc  19075  llycmpkgen2  19098  1stckgenlem  19101  kgencn2  19105  kgencn3  19106  ptbasfi  19129  ptpjopn  19160  txdis1cn  19183  txlly  19184  txnlly  19185  txtube  19188  txcmplem2  19190  tx1stc  19198  txkgen  19200  xkopt  19203  xkoco2cn  19206  xkococnlem  19207  xkococn  19208  xkoinjcn  19235  tgqtop  19260  regr1lem  19287  kqreglem1  19289  nrmhmph  19342  rnelfmlem  19500  rnelfm  19501  fmfnfmlem4  19505  fmfnfm  19506  ufldom  19510  flimopn  19523  hauspwpwf1  19535  fclsopn  19562  fclsnei  19567  fclsrest  19572  alexsublem  19591  alexsubALTlem3  19596  ptcmplem2  19600  ptcmplem3  19601  cnextfun  19611  cnextcn  19614  symgtgp  19647  tgpt0  19664  divstgpopn  19665  tsmsxplem1  19702  trust  19779  utopsnneiplem  19797  utop3cls  19801  utopreg  19802  isucn2  19829  cstucnd  19834  ucncn  19835  fmucnd  19842  cfilufg  19843  neipcfilu  19846  met2ndci  20072  prdsxmslem2  20079  metcnp3  20090  metustidOLD  20109  metustid  20110  metustexhalfOLD  20113  metustexhalf  20114  metustOLD  20117  metust  20118  metutopOLD  20132  psmetutop  20133  nmoleub  20285  reconnlem2  20379  xrge0tsms  20386  cncfco  20458  lebnumlem3  20510  lebnum  20511  nmoleub2lem2  20646  nmoleub3  20649  iscfil2  20752  iscau4  20765  iscmet3lem2  20778  equivcfil  20785  equivcau  20786  caubl  20793  rrxdstprj1  20883  ovolshftlem2  20968  ovolicc2lem4  20978  uniioombl  21044  i1fmulclem  21155  mbfi1fseqlem6  21173  itg2const2  21194  itg2split  21202  ellimc2  21327  ellimc3  21329  limcflf  21331  dvmptfsum  21422  dvferm1  21432  dvferm2  21434  dvlip2  21442  c1lip1  21444  lhop1  21461  ftc1a  21484  ply1divex  21583  plyeq0lem  21653  plymullem1  21657  coemullem  21692  coemulc  21697  ulmshftlem  21829  ulmcaulem  21834  ulmbdd  21838  ulmcn  21839  ulmdvlem3  21842  mtestbdd  21845  pserulm  21862  pserdvlem2  21868  abelthlem8  21879  xrlimcnp  22337  jensen  22357  logfac2  22531  dchrelbas3  22552  dchrpt  22581  lgsquad3  22675  2sqb  22692  rpvmasumlem  22711  dchrisumlem1  22713  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasumlem2  22722  dchrisum0flblem1  22732  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0  22744  mulog2sumlem2  22759  pntlem3  22833  ostth3  22862  istrkgcb  22894  tgbtwndiff  22934  tgcgrxfr  22945  lnext  22970  tgbtwnconn1  22978  tgbtwnconn3  22980  legval  22986  legtrid  22993  tglineeltr  23007  colline  23020  tglowdim2l  23021  mirreu3  23026  krippenlem  23049  midexlem  23051  f1otrg  23068  f1otrge  23069  axeuclidlem  23159  axcontlem2  23162  usgraidx2vlem2  23261  usgrares1  23274  nbgraf1olem5  23305  constr3cycl  23498  eupath2  23552  isgrp2d  23673  ubthlem3  24224  chirredlem1  25745  chirredlem3  25747  cdj1i  25788  xrge0infss  26004  omndmul2  26126  submarchi  26154  gsumle  26197  xrge0tsmsd  26204  suborng  26234  isarchiofld  26236  ordtrest2NEWlem  26304  ordtconlem1  26306  lmdvg  26335  esumpcvgval  26479  volmeas  26599  imambfm  26629  sgnmul  26877  signsply0  26904  signstres  26928  lgamucov  26976  erdszelem8  27038  pconcon  27072  cvmlift2lem12  27155  cvmlift3lem5  27164  cvmlift3lem7  27166  cvmlift3lem8  27167  nodenselem5  27777  btwnconn1lem13  28081  ltflcei  28372  lxflflp1  28374  heicant  28379  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  cnambfre  28393  itg2addnclem  28396  itg2addnclem2  28397  itg2gt0cn  28400  bddiblnc  28415  ftc1cnnc  28419  ftc1anclem5  28424  ftc1anclem7  28426  ftc1anc  28428  elicc3  28465  locfincmp  28529  neibastop2lem  28534  sstotbnd2  28626  equivtotbnd  28630  isbndx  28634  ssbnd  28640  heibor1lem  28661  rrncmslem  28684  elrfi  28983  eldioph2  29053  diophin  29064  irrapxlem2  29117  irrapxlem3  29118  irrapxlem4  29119  irrapxlem5  29120  pell1234qrne0  29147  pell1234qrreccl  29148  pell1234qrmulcl  29149  pell14qrgt0  29153  pell1234qrdich  29155  pell14qrdich  29163  pell1qrge1  29164  pellfundex  29180  congabseq  29270  jm2.27b  29308  jm2.27  29310  fnwe2lem2  29357  kelac1  29369  lnrfg  29428  hbt  29439  cntzsdrg  29512  stoweidlem31  29779  usgra2pthspth  30248  usgra2wlkspth  30251  clwlkisclwwlklem1  30402  wwlkext2clwwlk  30418  frisusgranb  30542  frgra2v  30544  frgra3vlem2  30546  2pthfrgrarn2  30555  usg2spot2nb  30611  usgreghash2spotv  30612  numclwwlk2lem1  30648  dmatsubcl  30800  pmatcollpw2lem  30820  mdetdiaglem  30824  lincsum  30852  lcoss  30859  snlindsntor  30894  islindeps2  30906  ad5ant12  31054  sineq0ALT  31560  islshpat  32502  lfl1dim  32606  lfl1dim2N  32607  lkrpssN  32648  glbconN  32861  hlhgt2  32873  3dim2  32952  3dim3  32953  islln3  32994  islvol5  33063  2lplnja  33103  dalem19  33166  isline4N  33261  2polssN  33399  lhpmatb  33515  4atex  33560  trlatn0  33656  cdlemf2  34046  dialss  34531  diaglbN  34540  diaintclN  34543  dibglbN  34651  dibintclN  34652  dihlsscpre  34719  dihglblem5aN  34777  dihglblem2aN  34778  dihglblem4  34782  dihatexv  34823  dihjat1lem  34913  lcfl6  34985  mapdval2N  35115
  Copyright terms: Public domain W3C validator