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

Theorem ad3antrrr 741
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 471 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 737 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ad4antr  743  ad5ant12  1250  fsnex  6206  oaabs  7371  oaabs2  7372  omabs  7374  undom  7686  sbthlem8  7715  findcard3  7840  cantnfle  8202  cantnfp1  8212  cantnflem1c  8218  sornom  8733  enfin2i  8777  ttukeylem6  8970  fpwwe2lem13  9093  fpwwe2  9094  winalim2  9147  wuncval2  9198  negf1o  10077  xlemul1a  11603  difreicc  11793  flflp1  12075  faclbnd  12507  swrdswrd  12853  swrdccatin12lem3  12883  swrdccat3blem  12888  ello12  13629  lo1bdd2  13637  elo12  13640  rlimclim1  13658  rlimcld2  13691  o1co  13699  o1of2  13725  o1rlimmul  13731  rlimsqzlem  13761  isercoll  13780  o1fsum  13922  supcvg  13963  dvds2ln  14382  lcmgcdlem  14620  isprm5  14700  pcadd  14883  vdwlem2  14981  vdwlem11  14990  prmdvdsprmorpOLD  15065  sbcie3s  15216  prdsval  15402  mreexexlem4d  15602  isacs2  15608  catcocl  15640  catass  15641  subccocl  15799  fullsubc  15804  funcco  15825  funcpropd  15854  fullpropd  15874  ffthiso  15883  isnat  15901  natpropd  15930  fucpropd  15931  xpcval  16111  evlf2  16152  curfpropd  16167  curfuncf  16172  uncfcurf  16173  curf2ndf  16181  hofcl  16193  hofpropd  16201  yonffthlem  16216  isacs3lem  16461  acsfiindd  16472  gsumpropd2lem  16565  resmhm2b  16657  mhmid  16856  mhmmnd  16857  ghmgrp  16859  conjnmzb  16966  pgpfi  17306  sylow3lem2  17329  efgredlem  17446  frgpnabllem1  17558  dprdfcntz  17697  ablfac1b  17752  pgpfac1lem3  17759  pgpfac1lem5  17761  pgpfaclem3  17765  islmhm2  18310  lspsneleq  18387  psrval  18635  psrass1  18678  resspsrmul  18690  mplbas2  18743  coe1tmmul  18919  gsummoncoe1  18947  znunit  19183  psgndiflemB  19217  uvcff  19398  uvcf1  19399  lindfmm  19434  dmatsubcl  19572  scmatscm  19587  smatvscl  19598  marrepval  19636  mdetdiaglem  19672  mdetunilem8  19693  mdetunilem9  19694  pmatcoe1fsupp  19774  decpmatmulsumfsupp  19846  pmatcollpw2lem  19850  mp2pm2mplem4  19882  pm2mpmhmlem1  19891  pm2mpmhmlem2  19892  pm2mp  19898  fvmptnn04if  19922  cpmadugsumfi  19950  cpmidg2sum  19953  cpmadumatpoly  19956  cayhamlem4  19961  neiptoptop  20196  neitr  20245  ordtrest2lem  20268  cnpnei  20329  iscncl  20334  cncls  20339  cnntr  20340  cncnp  20345  lmcnp  20369  isreg2  20442  hauscmplem  20470  cmpfi  20472  1stcfb  20509  1stcrest  20517  2ndcctbss  20519  2ndcomap  20522  islly2  20548  cldllycmp  20559  lly1stc  20560  locfincmp  20590  llycmpkgen2  20614  1stckgenlem  20617  kgencn2  20621  kgencn3  20622  ptbasfi  20645  ptpjopn  20676  txdis1cn  20699  txlly  20700  txnlly  20701  txtube  20704  txcmplem2  20706  tx1stc  20714  txkgen  20716  xkopt  20719  xkoco2cn  20722  xkococnlem  20723  xkococn  20724  xkoinjcn  20751  tgqtop  20776  regr1lem  20803  kqreglem1  20805  nrmhmph  20858  rnelfmlem  21016  rnelfm  21017  fmfnfmlem4  21021  fmfnfm  21022  ufldom  21026  flimopn  21039  hauspwpwf1  21051  fclsopn  21078  fclsnei  21083  fclsrest  21088  alexsublem  21108  alexsubALTlem3  21113  ptcmplem2  21117  ptcmplem3  21118  cnextfun  21128  cnextcn  21131  symgtgp  21165  tgpt0  21182  qustgpopn  21183  tsmsxplem1  21216  trust  21293  utopsnneiplem  21311  utop3cls  21315  utopreg  21316  isucn2  21343  cstucnd  21348  ucncn  21349  fmucnd  21356  cfilufg  21357  neipcfilu  21360  met2ndci  21586  prdsxmslem2  21593  metcnp3  21604  metustid  21618  metustexhalf  21620  metust  21622  psmetutop  21631  nmoleub  21785  nmoleubOLD  21801  reconnlem2  21894  xrge0tsms  21901  cncfco  21988  lebnumlem3  22040  lebnumlem3OLD  22043  lebnum  22044  nmoleub2lem2  22179  nmoleub3  22182  iscfil2  22285  iscau4  22298  iscmet3lem2  22311  equivcfil  22318  equivcau  22319  caubl  22326  rrxdstprj1  22412  ovolshftlem2  22512  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  uniioombl  22596  i1fmulclem  22709  mbfi1fseqlem6  22727  itg2const2  22748  itg2split  22756  ellimc2  22881  ellimc3  22883  limcflf  22885  dvmptfsum  22976  dvferm1  22986  dvferm2  22988  dvlip2  22996  c1lip1  22998  lhop1  23015  ftc1a  23038  ply1divex  23136  plyeq0lem  23213  plymullem1  23217  coemullem  23253  coemulc  23258  ulmshftlem  23393  ulmcaulem  23398  ulmbdd  23402  ulmcn  23403  ulmdvlem3  23406  mtestbdd  23409  pserulm  23426  pserdvlem2  23432  abelthlem8  23443  xrlimcnp  23943  jensen  23963  lgamucov  24012  logfac2  24194  dchrelbas3  24215  dchrpt  24244  lgsquad3  24338  2sqb  24355  rpvmasumlem  24374  dchrisumlem1  24376  dchrisumlem3  24378  dchrmusum2  24381  dchrvmasumlem2  24385  dchrisum0flblem1  24395  dchrisum0lem1b  24402  dchrisum0lem1  24403  dchrisum0  24407  mulog2sumlem2  24422  pntlem3  24496  ostth3  24525  istrkgcb  24553  tgbtwndiff  24599  iscgrglt  24608  tgcgrxfr  24612  motcgrg  24638  lnext  24661  tgbtwnconn1  24669  tgbtwnconn3  24671  legval  24678  legtrid  24685  legso  24693  hlcgreu  24712  tglnne  24722  tglineeltr  24725  tglnne0  24734  colline  24743  tglowdim2l  24744  tglowdim2ln  24745  mirreu3  24748  mirbtwnhl  24774  krippenlem  24784  midexlem  24786  perpcom  24807  perpneq  24808  footex  24812  colperpexlem3  24823  colperpex  24824  opphllem  24826  midex  24828  oppne3  24834  opptgdim2  24836  oppnid  24837  opphllem2  24839  opphllem5  24842  opphllem6  24843  oppperpex  24844  outpasch  24846  hlpasch  24847  lnopp2hpgb  24854  hpgerlem  24856  colopp  24860  colhp  24861  lmieu  24875  lnperpex  24894  trgcopy  24895  trgcopyeulem  24896  iscgra1  24901  cgrane1  24903  cgrane2  24904  cgrane3  24905  cgrane4  24906  cgrahl1  24907  cgrahl2  24908  cgracgr  24909  cgraswap  24911  cgracom  24913  cgratr  24914  cgrabtwn  24916  cgrahl  24917  sacgr  24921  acopyeu  24924  cgrg3col4  24933  tgasa1  24938  f1otrg  24950  f1otrge  24951  axeuclidlem  25041  axcontlem2  25044  usgraidx2vlem2  25168  usgrares1  25187  nbgraf1olem5  25222  usgra2wlkspth  25398  constr3cycl  25438  clwlkisclwwlklem1  25564  wwlkext2clwwlk  25580  eupath2  25757  frisusgranb  25774  frgra2v  25776  frgra3vlem2  25778  2pthfrgrarn2  25787  2spotiundisj  25839  usg2spot2nb  25842  usgreghash2spotv  25843  numclwwlk2lem1  25879  isgrp2d  26012  ubthlem3  26563  chirredlem1  28092  chirredlem3  28094  cdj1i  28135  xrge0infss  28389  xrge0infssOLD  28390  omndmul2  28524  submarchi  28552  gsumle  28591  xrge0tsmsd  28597  suborng  28627  isarchiofld  28629  psgnfzto1stlem  28662  fzto1st1  28664  smatrcl  28671  1smat1  28679  submateq  28684  mdetpmtr1  28698  madjusmdetlem2  28703  fimaproj  28709  locfinreflem  28716  cmppcmp  28734  ordtrest2NEWlem  28777  ordtconlem1  28779  lmdvg  28808  esumpcvgval  28948  esum2d  28963  sigapildsys  29033  ldgenpisyslem1  29034  fiunelros  29045  volmeas  29103  imambfm  29133  omssubadd  29177  omssubaddOLD  29181  carsggect  29199  carsgclctunlem3  29201  sgnmul  29462  signsply0  29489  signstres  29513  erdszelem8  29970  pconcon  30003  cvmlift2lem12  30086  cvmlift3lem5  30095  cvmlift3lem7  30097  cvmlift3lem8  30098  mrsubrn  30200  msrval  30225  msubff1  30243  nodenselem5  30623  btwnconn1lem13  30915  elicc3  31022  neibastop2lem  31065  ltflcei  31978  poimirlem4  31989  poimirlem13  31998  poimirlem14  31999  poimirlem22  32007  poimirlem26  32011  poimirlem27  32012  heicant  32020  mblfinlem2  32023  mblfinlem3  32024  mblfinlem4  32025  cnambfre  32034  itg2addnclem  32038  itg2addnclem2  32039  itg2gt0cn  32042  bddiblnc  32057  ftc1cnnc  32061  ftc1anclem5  32066  ftc1anclem7  32068  ftc1anc  32070  equivtotbnd  32155  isbndx  32159  ssbnd  32165  heibor1lem  32186  rrncmslem  32209  islshpat  32628  lfl1dim  32732  lfl1dim2N  32733  lkrpssN  32774  glbconN  32987  hlhgt2  32999  3dim2  33078  3dim3  33079  islln3  33120  islvol5  33189  2lplnja  33229  dalem19  33292  isline4N  33387  2polssN  33525  lhpmatb  33641  4atex  33686  trlatn0  33783  cdlemf2  34174  dialss  34659  diaglbN  34668  diaintclN  34671  dibglbN  34779  dibintclN  34780  dihlsscpre  34847  dihglblem5aN  34905  dihglblem2aN  34906  dihglblem4  34910  dihatexv  34951  dihjat1lem  35041  lcfl6  35113  mapdval2N  35243  elrfi  35581  eldioph2  35649  diophin  35660  irrapxlem2  35712  irrapxlem3  35713  irrapxlem4  35714  irrapxlem5  35715  pell1234qrne0  35744  pell1234qrreccl  35745  pell1234qrmulcl  35746  pell14qrgt0  35750  pell14qrdich  35760  pell1qrge1  35761  pellfundex  35779  congabseq  35869  jm2.27b  35906  jm2.27  35908  fnwe2lem2  35954  kelac1  35966  lnrfg  36023  hbt  36034  cntzsdrg  36113  cvgdvgrat  36706  binomcxplemnotnn0  36749  sineq0ALT  37374  disjf1  37495  supxrgere  37594  supxrgelem  37598  supxrge  37599  suplesup  37600  xralrple2  37615  mccl  37716  limcrecl  37747  lptioo2  37749  lptioo1  37750  lptre2pt  37758  addlimc  37767  icccncfext  37803  cncfiooicclem1  37809  cncfiooiccre  37811  dvbdfbdioolem2  37839  ioodvbdlimc1lem1  37841  ioodvbdlimc1lem1OLD  37843  dvnxpaek  37855  dvmptfprodlem  37857  dvmptfprod  37858  dvnprodlem3  37861  itgioocnicc  37892  itgspltprt  37894  stoweidlem31  37930  fourierdlem39  38047  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem48  38056  fourierdlem49  38057  fourierdlem50  38058  fourierdlem51  38059  fourierdlem64  38072  fourierdlem65  38073  fourierdlem74  38082  fourierdlem75  38083  fourierdlem81  38089  fourierdlem82  38090  fourierdlem101  38109  etransclem23  38160  etransclem27  38164  etransclem32  38169  etransclem33  38170  etransclem35  38172  etransclem38  38175  sge0tsms  38260  sge0cl  38261  sge0f1o  38262  sge0split  38289  sge0rpcpnf  38301  nnfoctbdjlem  38331  iundjiun  38336  omeiunltfirp  38378  carageniuncllem2  38381  carageniuncl  38382  hoidmv1lelem1  38451  hoidmvlelem3  38457  hoidmvlelem5  38459  hoidmvle  38460  hoiqssbllem3  38484  iccpartigtl  38775  iccpartgt  38779  bgoldbst  38917  bgoldbtbndlem4  38941  proththd  38952  usgredg2vlem2  39353  nbgr2vtx1edg  39468  nbuhgr2vtx1edgb  39470  3cycld  39919  usgra2pthspth  39938  usgvad2edg  39996  resmgmhm2b  40073  2zrngmmgm  40219  cznrng  40230  rnghmsubcsetclem2  40251  rhmsubcsetclem2  40297  srhmsubc  40351  rhmsubclem4  40364  srhmsubcALTV  40370  rhmsubcALTVlem4  40383  lincsum  40495  lcoss  40502  snlindsntor  40537  islindeps2  40549
  Copyright terms: Public domain W3C validator