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

Theorem ad3antrrr 734
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 466 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 730 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ad4antr  736  ad5ant12  1238  fsnex  6196  oaabs  7353  oaabs2  7354  omabs  7356  undom  7666  sbthlem8  7695  findcard3  7820  cantnfle  8175  cantnfp1  8185  cantnflem1c  8191  sornom  8705  enfin2i  8749  ttukeylem6  8942  fpwwe2lem13  9066  fpwwe2  9067  winalim2  9120  wuncval2  9171  negf1o  10048  xlemul1a  11574  difreicc  11762  flflp1  12040  faclbnd  12472  swrdswrd  12801  swrdccatin12lem3  12831  swrdccat3blem  12836  ello12  13558  lo1bdd2  13566  elo12  13569  rlimclim1  13587  rlimcld2  13620  o1co  13628  o1of2  13654  o1rlimmul  13660  rlimsqzlem  13690  isercoll  13709  o1fsum  13851  supcvg  13892  dvds2ln  14311  lcmgcdlem  14536  isprm5  14613  pcadd  14788  vdwlem2  14886  vdwlem11  14895  prmdvdsprmorpOLD  14970  sbcie3s  15121  prdsval  15303  mreexexlem4d  15495  isacs2  15501  catcocl  15533  catass  15534  subccocl  15692  fullsubc  15697  funcco  15718  funcpropd  15747  fullpropd  15767  ffthiso  15776  isnat  15794  natpropd  15823  fucpropd  15824  xpcval  16004  evlf2  16045  curfpropd  16060  curfuncf  16065  uncfcurf  16066  curf2ndf  16074  hofcl  16086  hofpropd  16094  yonffthlem  16109  isacs3lem  16354  acsfiindd  16365  gsumpropd2lem  16458  resmhm2b  16550  mhmid  16749  mhmmnd  16750  ghmgrp  16752  conjnmzb  16859  pgpfi  17183  sylow3lem2  17206  efgredlem  17323  frgpnabllem1  17435  dprdfcntz  17574  ablfac1b  17629  pgpfac1lem3  17636  pgpfac1lem5  17638  pgpfaclem3  17642  islmhm2  18187  lspsneleq  18264  psrval  18512  psrass1  18555  resspsrmul  18567  mplbas2  18620  coe1tmmul  18796  gsummoncoe1  18824  znunit  19056  psgndiflemB  19090  uvcff  19271  uvcf1  19272  lindfmm  19307  dmatsubcl  19445  scmatscm  19460  smatvscl  19471  marrepval  19509  mdetdiaglem  19545  mdetunilem8  19566  mdetunilem9  19567  pmatcoe1fsupp  19647  decpmatmulsumfsupp  19719  pmatcollpw2lem  19723  mp2pm2mplem4  19755  pm2mpmhmlem1  19764  pm2mpmhmlem2  19765  pm2mp  19771  fvmptnn04if  19795  cpmadugsumfi  19823  cpmidg2sum  19826  cpmadumatpoly  19829  cayhamlem4  19834  neiptoptop  20069  neitr  20118  ordtrest2lem  20141  cnpnei  20202  iscncl  20207  cncls  20212  cnntr  20213  cncnp  20218  lmcnp  20242  isreg2  20315  hauscmplem  20343  cmpfi  20345  1stcfb  20382  1stcrest  20390  2ndcctbss  20392  2ndcomap  20395  islly2  20421  cldllycmp  20432  lly1stc  20433  locfincmp  20463  llycmpkgen2  20487  1stckgenlem  20490  kgencn2  20494  kgencn3  20495  ptbasfi  20518  ptpjopn  20549  txdis1cn  20572  txlly  20573  txnlly  20574  txtube  20577  txcmplem2  20579  tx1stc  20587  txkgen  20589  xkopt  20592  xkoco2cn  20595  xkococnlem  20596  xkococn  20597  xkoinjcn  20624  tgqtop  20649  regr1lem  20676  kqreglem1  20678  nrmhmph  20731  rnelfmlem  20889  rnelfm  20890  fmfnfmlem4  20894  fmfnfm  20895  ufldom  20899  flimopn  20912  hauspwpwf1  20924  fclsopn  20951  fclsnei  20956  fclsrest  20961  alexsublem  20981  alexsubALTlem3  20986  ptcmplem2  20990  ptcmplem3  20991  cnextfun  21001  cnextcn  21004  symgtgp  21038  tgpt0  21055  qustgpopn  21056  tsmsxplem1  21089  trust  21166  utopsnneiplem  21184  utop3cls  21188  utopreg  21189  isucn2  21216  cstucnd  21221  ucncn  21222  fmucnd  21229  cfilufg  21230  neipcfilu  21233  met2ndci  21459  prdsxmslem2  21466  metcnp3  21477  metustid  21491  metustexhalf  21493  metust  21495  psmetutop  21504  nmoleub  21654  reconnlem2  21747  xrge0tsms  21754  cncfco  21826  lebnumlem3  21878  lebnum  21879  nmoleub2lem2  22014  nmoleub3  22017  iscfil2  22120  iscau4  22133  iscmet3lem2  22146  equivcfil  22153  equivcau  22154  caubl  22161  rrxdstprj1  22247  ovolshftlem2  22332  ovolicc2lem4  22342  uniioombl  22415  i1fmulclem  22528  mbfi1fseqlem6  22546  itg2const2  22567  itg2split  22575  ellimc2  22700  ellimc3  22702  limcflf  22704  dvmptfsum  22795  dvferm1  22805  dvferm2  22807  dvlip2  22815  c1lip1  22817  lhop1  22834  ftc1a  22857  ply1divex  22953  plyeq0lem  23023  plymullem1  23027  coemullem  23063  coemulc  23068  ulmshftlem  23200  ulmcaulem  23205  ulmbdd  23209  ulmcn  23210  ulmdvlem3  23213  mtestbdd  23216  pserulm  23233  pserdvlem2  23239  abelthlem8  23250  xrlimcnp  23750  jensen  23770  lgamucov  23819  logfac2  23999  dchrelbas3  24020  dchrpt  24049  lgsquad3  24143  2sqb  24160  rpvmasumlem  24179  dchrisumlem1  24181  dchrisumlem3  24183  dchrmusum2  24186  dchrvmasumlem2  24190  dchrisum0flblem1  24200  dchrisum0lem1b  24207  dchrisum0lem1  24208  dchrisum0  24212  mulog2sumlem2  24227  pntlem3  24301  ostth3  24330  istrkgcb  24358  tgbtwndiff  24404  tgcgrxfr  24416  motcgrg  24440  lnext  24463  tgbtwnconn1  24471  tgbtwnconn3  24473  legval  24480  legtrid  24487  legso  24495  hlcgreu  24513  tglnne  24523  tglineeltr  24526  tglnne0  24535  colline  24545  tglowdim2l  24546  tglowdim2ln  24547  mirreu3  24550  mirbtwnhl  24575  krippenlem  24583  midexlem  24585  perpcom  24606  perpneq  24607  footex  24611  colperpexlem3  24622  colperpex  24623  opphllem  24625  midex  24627  oppne3  24633  opptgdim2  24635  oppnid  24636  opphllem2  24638  opphllem5  24641  opphllem6  24642  oppperpex  24643  outpasch  24645  lnopp2hpgb  24652  hpgerlem  24654  colopp  24658  colhp  24659  lmieu  24673  lnperpex  24692  trgcopy  24693  trgcopyeulem  24694  iscgra1  24699  cgrane1  24701  cgrane2  24702  cgrane3  24703  cgrane4  24704  cgrahl1  24705  cgrahl2  24706  cgracgr  24707  cgraswap  24709  cgracom  24711  cgratr  24712  cgrabtwn  24713  cgrahl  24714  acopyeu  24719  tgasa1  24729  f1otrg  24738  f1otrge  24739  axeuclidlem  24829  axcontlem2  24832  usgraidx2vlem2  24956  usgrares1  24974  nbgraf1olem5  25009  usgra2wlkspth  25185  constr3cycl  25225  clwlkisclwwlklem1  25351  wwlkext2clwwlk  25367  eupath2  25544  frisusgranb  25561  frgra2v  25563  frgra3vlem2  25565  2pthfrgrarn2  25574  2spotiundisj  25626  usg2spot2nb  25629  usgreghash2spotv  25630  numclwwlk2lem1  25666  isgrp2d  25799  ubthlem3  26350  chirredlem1  27869  chirredlem3  27871  cdj1i  27912  xrge0infss  28172  omndmul2  28304  submarchi  28332  gsumle  28371  xrge0tsmsd  28378  suborng  28408  isarchiofld  28410  psgnfzto1stlem  28443  fzto1st1  28445  smatrcl  28452  1smat1  28460  submateq  28465  mdetpmtr1  28479  madjusmdetlem2  28484  fimaproj  28490  locfinreflem  28497  cmppcmp  28515  ordtrest2NEWlem  28558  ordtconlem1  28560  lmdvg  28589  esumpcvgval  28729  esum2d  28744  sigapildsys  28814  ldgenpisyslem1  28815  fiunelros  28826  volmeas  28884  imambfm  28914  omssubadd  28952  carsggect  28970  carsgclctunlem3  28972  sgnmul  29192  signsply0  29219  signstres  29243  erdszelem8  29700  pconcon  29733  cvmlift2lem12  29816  cvmlift3lem5  29825  cvmlift3lem7  29827  cvmlift3lem8  29828  mrsubrn  29930  msrval  29955  msubff1  29973  nodenselem5  30350  btwnconn1lem13  30642  elicc3  30749  neibastop2lem  30792  ltflcei  31627  poimirlem4  31638  poimirlem13  31647  poimirlem14  31648  poimirlem22  31656  poimirlem26  31660  poimirlem27  31661  heicant  31669  mblfinlem2  31672  mblfinlem3  31673  mblfinlem4  31674  cnambfre  31683  itg2addnclem  31687  itg2addnclem2  31688  itg2gt0cn  31691  bddiblnc  31706  ftc1cnnc  31710  ftc1anclem5  31715  ftc1anclem7  31717  ftc1anc  31719  equivtotbnd  31804  isbndx  31808  ssbnd  31814  heibor1lem  31835  rrncmslem  31858  islshpat  32282  lfl1dim  32386  lfl1dim2N  32387  lkrpssN  32428  glbconN  32641  hlhgt2  32653  3dim2  32732  3dim3  32733  islln3  32774  islvol5  32843  2lplnja  32883  dalem19  32946  isline4N  33041  2polssN  33179  lhpmatb  33295  4atex  33340  trlatn0  33437  cdlemf2  33828  dialss  34313  diaglbN  34322  diaintclN  34325  dibglbN  34433  dibintclN  34434  dihlsscpre  34501  dihglblem5aN  34559  dihglblem2aN  34560  dihglblem4  34564  dihatexv  34605  dihjat1lem  34695  lcfl6  34767  mapdval2N  34897  elrfi  35235  eldioph2  35303  diophin  35314  irrapxlem2  35367  irrapxlem3  35368  irrapxlem4  35369  irrapxlem5  35370  pell1234qrne0  35397  pell1234qrreccl  35398  pell1234qrmulcl  35399  pell14qrgt0  35403  pell14qrdich  35413  pell1qrge1  35414  pellfundex  35430  congabseq  35520  jm2.27b  35557  jm2.27  35559  fnwe2lem2  35605  kelac1  35617  lnrfg  35674  hbt  35685  cntzsdrg  35757  cvgdvgrat  36289  binomcxplemnotnn0  36332  sineq0ALT  36964  disjf1  37070  supxrgere  37155  supxrgelem  37159  supxrge  37160  suplesup  37161  mccl  37240  limcrecl  37271  lptioo2  37273  lptioo1  37274  lptre2pt  37282  addlimc  37291  icccncfext  37327  cncfiooicclem1  37333  cncfiooiccre  37335  dvbdfbdioolem2  37363  ioodvbdlimc1lem1  37365  dvnxpaek  37376  dvmptfprodlem  37378  dvmptfprod  37379  dvnprodlem3  37382  itgioocnicc  37413  itgspltprt  37415  stoweidlem31  37451  fourierdlem39  37567  fourierdlem42  37570  fourierdlem48  37576  fourierdlem49  37577  fourierdlem50  37578  fourierdlem51  37579  fourierdlem64  37592  fourierdlem65  37593  fourierdlem74  37602  fourierdlem75  37603  fourierdlem81  37609  fourierdlem82  37610  fourierdlem101  37629  etransclem23  37679  etransclem27  37683  etransclem32  37688  etransclem33  37689  etransclem35  37691  etransclem38  37694  sge0tsms  37746  sge0cl  37747  sge0f1o  37748  sge0split  37775  nnfoctbdjlem  37792  iundjiun  37797  omeiunltfirp  37839  carageniuncllem2  37842  carageniuncl  37843  iccpartigtl  38117  iccpartgt  38121  bgoldbst  38259  bgoldbtbndlem4  38283  proththd  38294  usgra2pthspth  38411  usgvad2edg  38471  resmgmhm2b  38548  2zrngmmgm  38694  cznrng  38705  rnghmsubcsetclem2  38726  rhmsubcsetclem2  38772  srhmsubc  38826  rhmsubclem4  38839  srhmsubcALTV  38845  rhmsubcALTVlem4  38858  lincsum  38972  lcoss  38979  snlindsntor  39014  islindeps2  39026
  Copyright terms: Public domain W3C validator