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

Theorem ad3antrrr 722
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 462 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 718 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  724  oaabs  7071  oaabs2  7072  omabs  7074  undom  7387  sbthlem8  7416  findcard3  7543  cantnfle  7867  cantnfp1  7877  cantnflem1c  7883  cantnfleOLD  7897  cantnfp1OLD  7903  cantnflem1cOLD  7906  sornom  8434  enfin2i  8478  ttukeylem6  8671  fpwwe2lem13  8797  fpwwe2  8798  winalim2  8851  wuncval2  8902  xlemul1a  11239  difreicc  11404  faclbnd  12050  swrdswrd  12338  swrdccatin12lem3  12365  swrdccat3blem  12370  ello12  12978  lo1bdd2  12986  elo12  12989  rlimclim1  13007  rlimcld2  13040  o1co  13048  o1of2  13074  o1rlimmul  13080  rlimsqzlem  13110  isercoll  13129  o1fsum  13259  supcvg  13301  dvds2ln  13546  isprm5  13781  pcadd  13934  vdwlem2  14026  vdwlem11  14035  sbcie3s  14201  prdsval  14376  mreexexlem4d  14568  isacs2  14574  catcocl  14606  catass  14607  subccocl  14738  fullsubc  14743  funcco  14764  funcpropd  14793  fullpropd  14813  ffthiso  14822  isnat  14840  natpropd  14869  fucpropd  14870  xpcval  14970  evlf2  15011  curfpropd  15026  curfuncf  15031  uncfcurf  15032  curf2ndf  15040  hofcl  15052  hofpropd  15060  yonffthlem  15075  isacs3lem  15319  acsfiindd  15330  resmhm2b  15471  conjnmzb  15761  pgpfi  16084  sylow3lem2  16107  efgredlem  16224  frgpnabllem1  16331  dprdfcntz  16473  dprdfcntzOLD  16479  ablfac1b  16545  pgpfac1lem3  16552  pgpfac1lem5  16554  pgpfaclem3  16558  islmhm2  17041  lspsneleq  17118  psrval  17363  psrass1  17412  resspsrmul  17423  mplbas2  17483  mplbas2OLD  17484  coe1tmmul  17628  znunit  17838  psgndiflemB  17872  uvcff  18058  uvcf1  18059  lindfmm  18098  marrepval  18215  mdetunilem8  18267  mdetunilem9  18268  neiptoptop  18577  neitr  18626  ordtrest2lem  18649  cnpnei  18710  iscncl  18715  cncls  18720  cnntr  18721  cncnp  18726  lmcnp  18750  isreg2  18823  hauscmplem  18851  cmpfi  18853  1stcfb  18891  1stcrest  18899  2ndcctbss  18901  2ndcomap  18904  islly2  18930  cldllycmp  18941  lly1stc  18942  llycmpkgen2  18965  1stckgenlem  18968  kgencn2  18972  kgencn3  18973  ptbasfi  18996  ptpjopn  19027  txdis1cn  19050  txlly  19051  txnlly  19052  txtube  19055  txcmplem2  19057  tx1stc  19065  txkgen  19067  xkopt  19070  xkoco2cn  19073  xkococnlem  19074  xkococn  19075  xkoinjcn  19102  tgqtop  19127  regr1lem  19154  kqreglem1  19156  nrmhmph  19209  rnelfmlem  19367  rnelfm  19368  fmfnfmlem4  19372  fmfnfm  19373  ufldom  19377  flimopn  19390  hauspwpwf1  19402  fclsopn  19429  fclsnei  19434  fclsrest  19439  alexsublem  19458  alexsubALTlem3  19463  ptcmplem2  19467  ptcmplem3  19468  cnextfun  19478  cnextcn  19481  symgtgp  19514  tgpt0  19531  divstgpopn  19532  tsmsxplem1  19569  trust  19646  utopsnneiplem  19664  utop3cls  19668  utopreg  19669  isucn2  19696  cstucnd  19701  ucncn  19702  fmucnd  19709  cfilufg  19710  neipcfilu  19713  met2ndci  19939  prdsxmslem2  19946  metcnp3  19957  metustidOLD  19976  metustid  19977  metustexhalfOLD  19980  metustexhalf  19981  metustOLD  19984  metust  19985  metutopOLD  19999  psmetutop  20000  nmoleub  20152  reconnlem2  20246  xrge0tsms  20253  cncfco  20325  lebnumlem3  20377  lebnum  20378  nmoleub2lem2  20513  nmoleub3  20516  iscfil2  20619  iscau4  20632  iscmet3lem2  20645  equivcfil  20652  equivcau  20653  caubl  20660  rrxdstprj1  20750  ovolshftlem2  20835  ovolicc2lem4  20845  uniioombl  20911  i1fmulclem  21022  mbfi1fseqlem6  21040  itg2const2  21061  itg2split  21069  ellimc2  21194  ellimc3  21196  limcflf  21198  dvmptfsum  21289  dvferm1  21299  dvferm2  21301  dvlip2  21309  c1lip1  21311  lhop1  21328  ftc1a  21351  ply1divex  21493  plyeq0lem  21563  plymullem1  21567  coemullem  21602  coemulc  21607  ulmshftlem  21739  ulmcaulem  21744  ulmbdd  21748  ulmcn  21749  ulmdvlem3  21752  mtestbdd  21755  pserulm  21772  pserdvlem2  21778  abelthlem8  21789  xrlimcnp  22247  jensen  22267  logfac2  22441  dchrelbas3  22462  dchrpt  22491  lgsquad3  22585  2sqb  22602  rpvmasumlem  22621  dchrisumlem1  22623  dchrisumlem3  22625  dchrmusum2  22628  dchrvmasumlem2  22632  dchrisum0flblem1  22642  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0  22654  mulog2sumlem2  22669  pntlem3  22743  ostth3  22772  istrkgcb  22804  tgbtwndiff  22841  tgcgrxfr  22851  lnext  22875  tgbtwnconn1  22883  tgbtwnconn3  22885  legval  22891  legtrid  22898  tglineeltr  22908  colline  22918  tglowdim2l  22919  mirreu3  22924  f1otrg  22940  f1otrge  22941  axeuclidlem  23031  axcontlem2  23034  usgraidx2vlem2  23133  usgrares1  23146  nbgraf1olem5  23177  constr3cycl  23370  eupath2  23424  isgrp2d  23545  ubthlem3  24096  chirredlem1  25617  chirredlem3  25619  cdj1i  25660  omndmul2  25999  submarchi  26027  gsumpropd2lem  26093  gsumle  26098  xrge0tsmsd  26106  suborng  26136  isarchiofld  26138  ordtrest2NEWlem  26206  ordtconlem1  26208  lmdvg  26237  esumpcvgval  26381  volmeas  26501  imambfm  26531  sgnmul  26773  signsply0  26800  signstres  26824  lgamucov  26872  erdszelem8  26934  pconcon  26968  cvmlift2lem12  27051  cvmlift3lem5  27060  cvmlift3lem7  27062  cvmlift3lem8  27063  nodenselem5  27673  btwnconn1lem13  27977  ltflcei  28263  lxflflp1  28265  heicant  28270  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  cnambfre  28284  itg2addnclem  28287  itg2addnclem2  28288  itg2gt0cn  28291  bddiblnc  28306  ftc1cnnc  28310  ftc1anclem5  28315  ftc1anclem7  28317  ftc1anc  28319  elicc3  28356  locfincmp  28420  neibastop2lem  28425  sstotbnd2  28517  equivtotbnd  28521  isbndx  28525  ssbnd  28531  heibor1lem  28552  rrncmslem  28575  elrfi  28875  eldioph2  28945  diophin  28956  irrapxlem2  29009  irrapxlem3  29010  irrapxlem4  29011  irrapxlem5  29012  pell1234qrne0  29039  pell1234qrreccl  29040  pell1234qrmulcl  29041  pell14qrgt0  29045  pell1234qrdich  29047  pell14qrdich  29055  pell1qrge1  29056  pellfundex  29072  congabseq  29162  jm2.27b  29200  jm2.27  29202  fnwe2lem2  29249  kelac1  29261  lnrfg  29320  hbt  29331  cntzsdrg  29404  stoweidlem31  29672  usgra2pthspth  30141  usgra2wlkspth  30144  clwlkisclwwlklem1  30295  wwlkext2clwwlk  30311  frisusgranb  30435  frgra2v  30437  frgra3vlem2  30439  2pthfrgrarn2  30448  usg2spot2nb  30504  usgreghash2spotv  30505  numclwwlk2lem1  30541  lincsum  30672  lcoss  30679  snlindsntor  30714  islindeps2  30726  ad5ant12  30868  sineq0ALT  31375  islshpat  32235  lfl1dim  32339  lfl1dim2N  32340  lkrpssN  32381  glbconN  32594  hlhgt2  32606  3dim2  32685  3dim3  32686  islln3  32727  islvol5  32796  2lplnja  32836  dalem19  32899  isline4N  32994  2polssN  33132  lhpmatb  33248  4atex  33293  trlatn0  33389  cdlemf2  33779  dialss  34264  diaglbN  34273  diaintclN  34276  dibglbN  34384  dibintclN  34385  dihlsscpre  34452  dihglblem5aN  34510  dihglblem2aN  34511  dihglblem4  34515  dihatexv  34556  dihjat1lem  34646  lcfl6  34718  mapdval2N  34848
  Copyright terms: Public domain W3C validator