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  6135  oaabs  7295  oaabs2  7296  omabs  7298  undom  7608  sbthlem8  7637  findcard3  7762  cantnfle  8123  cantnfp1  8133  cantnflem1c  8139  sornom  8653  enfin2i  8697  ttukeylem6  8890  fpwwe2lem13  9013  fpwwe2  9014  winalim2  9067  wuncval2  9118  negf1o  9995  xlemul1a  11520  difreicc  11710  flflp1  11988  faclbnd  12420  swrdswrd  12757  swrdccatin12lem3  12787  swrdccat3blem  12792  ello12  13518  lo1bdd2  13526  elo12  13529  rlimclim1  13547  rlimcld2  13580  o1co  13588  o1of2  13614  o1rlimmul  13620  rlimsqzlem  13650  isercoll  13669  o1fsum  13811  supcvg  13852  dvds2ln  14271  lcmgcdlem  14509  isprm5  14589  pcadd  14772  vdwlem2  14870  vdwlem11  14879  prmdvdsprmorpOLD  14954  sbcie3s  15105  prdsval  15291  mreexexlem4d  15491  isacs2  15497  catcocl  15529  catass  15530  subccocl  15688  fullsubc  15693  funcco  15714  funcpropd  15743  fullpropd  15763  ffthiso  15772  isnat  15790  natpropd  15819  fucpropd  15820  xpcval  16000  evlf2  16041  curfpropd  16056  curfuncf  16061  uncfcurf  16062  curf2ndf  16070  hofcl  16082  hofpropd  16090  yonffthlem  16105  isacs3lem  16350  acsfiindd  16361  gsumpropd2lem  16454  resmhm2b  16546  mhmid  16745  mhmmnd  16746  ghmgrp  16748  conjnmzb  16855  pgpfi  17195  sylow3lem2  17218  efgredlem  17335  frgpnabllem1  17447  dprdfcntz  17586  ablfac1b  17641  pgpfac1lem3  17648  pgpfac1lem5  17650  pgpfaclem3  17654  islmhm2  18199  lspsneleq  18276  psrval  18524  psrass1  18567  resspsrmul  18579  mplbas2  18632  coe1tmmul  18808  gsummoncoe1  18836  znunit  19071  psgndiflemB  19105  uvcff  19286  uvcf1  19287  lindfmm  19322  dmatsubcl  19460  scmatscm  19475  smatvscl  19486  marrepval  19524  mdetdiaglem  19560  mdetunilem8  19581  mdetunilem9  19582  pmatcoe1fsupp  19662  decpmatmulsumfsupp  19734  pmatcollpw2lem  19738  mp2pm2mplem4  19770  pm2mpmhmlem1  19779  pm2mpmhmlem2  19780  pm2mp  19786  fvmptnn04if  19810  cpmadugsumfi  19838  cpmidg2sum  19841  cpmadumatpoly  19844  cayhamlem4  19849  neiptoptop  20084  neitr  20133  ordtrest2lem  20156  cnpnei  20217  iscncl  20222  cncls  20227  cnntr  20228  cncnp  20233  lmcnp  20257  isreg2  20330  hauscmplem  20358  cmpfi  20360  1stcfb  20397  1stcrest  20405  2ndcctbss  20407  2ndcomap  20410  islly2  20436  cldllycmp  20447  lly1stc  20448  locfincmp  20478  llycmpkgen2  20502  1stckgenlem  20505  kgencn2  20509  kgencn3  20510  ptbasfi  20533  ptpjopn  20564  txdis1cn  20587  txlly  20588  txnlly  20589  txtube  20592  txcmplem2  20594  tx1stc  20602  txkgen  20604  xkopt  20607  xkoco2cn  20610  xkococnlem  20611  xkococn  20612  xkoinjcn  20639  tgqtop  20664  regr1lem  20691  kqreglem1  20693  nrmhmph  20746  rnelfmlem  20904  rnelfm  20905  fmfnfmlem4  20909  fmfnfm  20910  ufldom  20914  flimopn  20927  hauspwpwf1  20939  fclsopn  20966  fclsnei  20971  fclsrest  20976  alexsublem  20996  alexsubALTlem3  21001  ptcmplem2  21005  ptcmplem3  21006  cnextfun  21016  cnextcn  21019  symgtgp  21053  tgpt0  21070  qustgpopn  21071  tsmsxplem1  21104  trust  21181  utopsnneiplem  21199  utop3cls  21203  utopreg  21204  isucn2  21231  cstucnd  21236  ucncn  21237  fmucnd  21244  cfilufg  21245  neipcfilu  21248  met2ndci  21474  prdsxmslem2  21481  metcnp3  21492  metustid  21506  metustexhalf  21508  metust  21510  psmetutop  21519  nmoleub  21673  nmoleubOLD  21689  reconnlem2  21782  xrge0tsms  21789  cncfco  21876  lebnumlem3  21928  lebnumlem3OLD  21931  lebnum  21932  nmoleub2lem2  22067  nmoleub3  22070  iscfil2  22173  iscau4  22186  iscmet3lem2  22199  equivcfil  22206  equivcau  22207  caubl  22214  rrxdstprj1  22300  ovolshftlem2  22400  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  uniioombl  22484  i1fmulclem  22597  mbfi1fseqlem6  22615  itg2const2  22636  itg2split  22644  ellimc2  22769  ellimc3  22771  limcflf  22773  dvmptfsum  22864  dvferm1  22874  dvferm2  22876  dvlip2  22884  c1lip1  22886  lhop1  22903  ftc1a  22926  ply1divex  23024  plyeq0lem  23101  plymullem1  23105  coemullem  23141  coemulc  23146  ulmshftlem  23281  ulmcaulem  23286  ulmbdd  23290  ulmcn  23291  ulmdvlem3  23294  mtestbdd  23297  pserulm  23314  pserdvlem2  23320  abelthlem8  23331  xrlimcnp  23831  jensen  23851  lgamucov  23900  logfac2  24082  dchrelbas3  24103  dchrpt  24132  lgsquad3  24226  2sqb  24243  rpvmasumlem  24262  dchrisumlem1  24264  dchrisumlem3  24266  dchrmusum2  24269  dchrvmasumlem2  24273  dchrisum0flblem1  24283  dchrisum0lem1b  24290  dchrisum0lem1  24291  dchrisum0  24295  mulog2sumlem2  24310  pntlem3  24384  ostth3  24413  istrkgcb  24441  tgbtwndiff  24487  iscgrglt  24496  tgcgrxfr  24500  motcgrg  24526  lnext  24549  tgbtwnconn1  24557  tgbtwnconn3  24559  legval  24566  legtrid  24573  legso  24581  hlcgreu  24600  tglnne  24610  tglineeltr  24613  tglnne0  24622  colline  24631  tglowdim2l  24632  tglowdim2ln  24633  mirreu3  24636  mirbtwnhl  24662  krippenlem  24672  midexlem  24674  perpcom  24695  perpneq  24696  footex  24700  colperpexlem3  24711  colperpex  24712  opphllem  24714  midex  24716  oppne3  24722  opptgdim2  24724  oppnid  24725  opphllem2  24727  opphllem5  24730  opphllem6  24731  oppperpex  24732  outpasch  24734  hlpasch  24735  lnopp2hpgb  24742  hpgerlem  24744  colopp  24748  colhp  24749  lmieu  24763  lnperpex  24782  trgcopy  24783  trgcopyeulem  24784  iscgra1  24789  cgrane1  24791  cgrane2  24792  cgrane3  24793  cgrane4  24794  cgrahl1  24795  cgrahl2  24796  cgracgr  24797  cgraswap  24799  cgracom  24801  cgratr  24802  cgrabtwn  24804  cgrahl  24805  sacgr  24809  acopyeu  24812  cgrg3col4  24821  tgasa1  24826  f1otrg  24838  f1otrge  24839  axeuclidlem  24929  axcontlem2  24932  usgraidx2vlem2  25056  usgrares1  25075  nbgraf1olem5  25110  usgra2wlkspth  25286  constr3cycl  25326  clwlkisclwwlklem1  25452  wwlkext2clwwlk  25468  eupath2  25645  frisusgranb  25662  frgra2v  25664  frgra3vlem2  25666  2pthfrgrarn2  25675  2spotiundisj  25727  usg2spot2nb  25730  usgreghash2spotv  25731  numclwwlk2lem1  25767  isgrp2d  25900  ubthlem3  26451  chirredlem1  27980  chirredlem3  27982  cdj1i  28023  xrge0infss  28285  xrge0infssOLD  28286  omndmul2  28421  submarchi  28449  gsumle  28488  xrge0tsmsd  28495  suborng  28525  isarchiofld  28527  psgnfzto1stlem  28560  fzto1st1  28562  smatrcl  28569  1smat1  28577  submateq  28582  mdetpmtr1  28596  madjusmdetlem2  28601  fimaproj  28607  locfinreflem  28614  cmppcmp  28632  ordtrest2NEWlem  28675  ordtconlem1  28677  lmdvg  28706  esumpcvgval  28846  esum2d  28861  sigapildsys  28931  ldgenpisyslem1  28932  fiunelros  28943  volmeas  29001  imambfm  29031  omssubadd  29075  omssubaddOLD  29079  carsggect  29097  carsgclctunlem3  29099  sgnmul  29360  signsply0  29387  signstres  29411  erdszelem8  29868  pconcon  29901  cvmlift2lem12  29984  cvmlift3lem5  29993  cvmlift3lem7  29995  cvmlift3lem8  29996  mrsubrn  30098  msrval  30123  msubff1  30141  nodenselem5  30518  btwnconn1lem13  30810  elicc3  30917  neibastop2lem  30960  ltflcei  31840  poimirlem4  31851  poimirlem13  31860  poimirlem14  31861  poimirlem22  31869  poimirlem26  31873  poimirlem27  31874  heicant  31882  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  cnambfre  31896  itg2addnclem  31900  itg2addnclem2  31901  itg2gt0cn  31904  bddiblnc  31919  ftc1cnnc  31923  ftc1anclem5  31928  ftc1anclem7  31930  ftc1anc  31932  equivtotbnd  32017  isbndx  32021  ssbnd  32027  heibor1lem  32048  rrncmslem  32071  islshpat  32495  lfl1dim  32599  lfl1dim2N  32600  lkrpssN  32641  glbconN  32854  hlhgt2  32866  3dim2  32945  3dim3  32946  islln3  32987  islvol5  33056  2lplnja  33096  dalem19  33159  isline4N  33254  2polssN  33392  lhpmatb  33508  4atex  33553  trlatn0  33650  cdlemf2  34041  dialss  34526  diaglbN  34535  diaintclN  34538  dibglbN  34646  dibintclN  34647  dihlsscpre  34714  dihglblem5aN  34772  dihglblem2aN  34773  dihglblem4  34777  dihatexv  34818  dihjat1lem  34908  lcfl6  34980  mapdval2N  35110  elrfi  35448  eldioph2  35516  diophin  35527  irrapxlem2  35580  irrapxlem3  35581  irrapxlem4  35582  irrapxlem5  35583  pell1234qrne0  35612  pell1234qrreccl  35613  pell1234qrmulcl  35614  pell14qrgt0  35618  pell14qrdich  35628  pell1qrge1  35629  pellfundex  35647  congabseq  35737  jm2.27b  35774  jm2.27  35776  fnwe2lem2  35822  kelac1  35834  lnrfg  35891  hbt  35902  cntzsdrg  35981  cvgdvgrat  36575  binomcxplemnotnn0  36618  sineq0ALT  37250  disjf1  37361  supxrgere  37453  supxrgelem  37457  supxrge  37458  suplesup  37459  xralrple2  37474  mccl  37561  limcrecl  37592  lptioo2  37594  lptioo1  37595  lptre2pt  37603  addlimc  37612  icccncfext  37648  cncfiooicclem1  37654  cncfiooiccre  37656  dvbdfbdioolem2  37684  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem1OLD  37688  dvnxpaek  37700  dvmptfprodlem  37702  dvmptfprod  37703  dvnprodlem3  37706  itgioocnicc  37737  itgspltprt  37739  stoweidlem31  37775  fourierdlem39  37892  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem51  37904  fourierdlem64  37917  fourierdlem65  37918  fourierdlem74  37927  fourierdlem75  37928  fourierdlem81  37934  fourierdlem82  37935  fourierdlem101  37954  etransclem23  38005  etransclem27  38009  etransclem32  38014  etransclem33  38015  etransclem35  38017  etransclem38  38020  sge0tsms  38073  sge0cl  38074  sge0f1o  38075  sge0split  38102  sge0rpcpnf  38114  nnfoctbdjlem  38144  iundjiun  38149  omeiunltfirp  38191  carageniuncllem2  38194  carageniuncl  38195  hoidmv1lelem1  38260  hoidmvlelem3  38266  hoidmvlelem5  38268  hoidmvle  38269  iccpartigtl  38550  iccpartgt  38554  bgoldbst  38692  bgoldbtbndlem4  38716  proththd  38727  usgridx2vlem2  39050  nbgr2vtx1edg  39154  nbuhgr2vtx1edgb  39156  usgra2pthspth  39256  usgvad2edg  39314  resmgmhm2b  39391  2zrngmmgm  39537  cznrng  39548  rnghmsubcsetclem2  39569  rhmsubcsetclem2  39615  srhmsubc  39669  rhmsubclem4  39682  srhmsubcALTV  39688  rhmsubcALTVlem4  39701  lincsum  39815  lcoss  39822  snlindsntor  39857  islindeps2  39869
  Copyright terms: Public domain W3C validator