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

Theorem ad3antrrr 710
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 451 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 706 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad4antr  712  oaabs  6658  oaabs2  6659  omabs  6661  undom  6966  sbthlem8  6994  findcard3  7116  marypha1lem  7202  cantnfle  7388  cantnfp1  7399  cantnflem1c  7405  sornom  7919  enfin2i  7963  ttukeylem6  8157  fpwwe2lem13  8280  fpwwe2  8281  winalim2  8334  wuncval2  8385  xlemul1a  10624  difreicc  10783  faclbnd  11319  ello12  12006  lo1bdd2  12014  elo12  12017  rlimclim1  12035  rlimcld2  12068  o1co  12076  o1of2  12102  o1rlimmul  12108  rlimsqzlem  12138  isercoll  12157  o1fsum  12287  supcvg  12330  dvds2ln  12575  isprm5  12807  pcadd  12953  vdwlem2  13045  vdwlem11  13054  prdsval  13371  mreexexlem4d  13565  isacs2  13571  catcocl  13603  catass  13604  catpropd  13628  subccocl  13735  fullsubc  13740  funcco  13761  funcpropd  13790  fullpropd  13810  ffthiso  13819  isnat  13837  natpropd  13866  fucpropd  13867  xpcval  13967  evlf2  14008  curfpropd  14023  curfuncf  14028  uncfcurf  14029  curf2ndf  14037  hofcl  14049  hofpropd  14057  yonffthlem  14072  drsdirfi  14088  isacs3lem  14285  acsfiindd  14296  resmhm2b  14454  conjnmzb  14733  pgpfi  14932  sylow3lem2  14955  efgredlem  15072  frgpnabllem1  15177  dprdfcntz  15266  ablfac1b  15321  pgpfac1lem3  15328  pgpfac1lem5  15330  pgpfaclem3  15334  islmhm2  15811  lspsneleq  15884  psrval  16126  psrass1  16166  resspsrmul  16177  mplbas2  16228  coe1tmmul  16369  znunit  16533  ordtrest2lem  16949  cnpnei  17009  iscncl  17014  cncls  17019  cnntr  17020  cncnp  17025  lmcnp  17048  isreg2  17121  hauscmplem  17149  cmpfi  17151  1stcfb  17187  1stcrest  17195  2ndcctbss  17197  2ndcomap  17200  islly2  17226  cldllycmp  17237  lly1stc  17238  llycmpkgen2  17261  1stckgenlem  17264  kgencn2  17268  kgencn3  17269  ptbasfi  17292  ptpjopn  17322  xkoccn  17329  txdis1cn  17345  txlly  17346  txnlly  17347  txtube  17350  txcmplem2  17352  tx1stc  17360  txkgen  17362  xkopt  17365  xkoco2cn  17368  xkococnlem  17369  xkococn  17370  xkoinjcn  17397  tgqtop  17419  regr1lem  17446  kqreglem1  17448  nrmhmph  17501  rnelfmlem  17663  rnelfm  17664  fmfnfmlem4  17668  fmfnfm  17669  ufldom  17673  flimopn  17686  hauspwpwf1  17698  fclsopn  17725  fclsnei  17730  fclsrest  17735  alexsublem  17754  alexsubALTlem3  17759  ptcmplem2  17763  ptcmplem3  17764  symgtgp  17800  tgpt0  17817  divstgpopn  17818  divstgplem  17819  tsmsxplem1  17851  met1stc  18083  met2ndci  18084  prdsxmslem2  18091  metcnp3  18102  nmoleub  18256  reconnlem2  18348  xrge0tsms  18355  cncfco  18427  cnheibor  18469  lebnumlem3  18477  lebnum  18478  nmoleub2lem2  18613  nmoleub3  18616  iscfil2  18708  iscau4  18721  iscmet3lem2  18734  equivcfil  18741  equivcau  18742  caubl  18749  ovolshftlem2  18885  ovolicc2lem4  18895  uniioombl  18960  i1fmulclem  19073  mbfi1fseqlem6  19091  itg2const2  19112  itg2split  19120  ellimc2  19243  ellimc3  19245  limcflf  19247  dvmptfsum  19338  dvferm1  19348  dvferm2  19350  dvlip2  19358  c1lip1  19360  lhop1  19377  ftc1a  19400  ply1divex  19538  plyeq0lem  19608  plymullem1  19612  coemullem  19647  coemulc  19652  ulmshftlem  19784  ulmcaulem  19787  ulmcau  19788  ulmbdd  19791  ulmcn  19792  ulmdvlem3  19795  pserulm  19814  pserdvlem2  19820  abelthlem8  19831  xrlimcnp  20279  jensen  20299  logfac2  20472  dchrelbas3  20493  dchrpt  20522  lgsquad3  20616  2sqb  20633  rpvmasumlem  20652  dchrisumlem1  20654  dchrisumlem3  20656  dchrmusum2  20659  dchrvmasumlem2  20663  dchrisum0flblem1  20673  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0  20685  mulog2sumlem2  20700  pntlem3  20774  ostth3  20803  isgrp2d  20918  ubthlem3  21467  chirredlem1  22986  chirredlem3  22988  cdj1i  23029  lmdvg  23391  gsumpropd2lem  23394  xrge0tsmsd  23397  esumcst  23451  esumpcvgval  23461  imambfm  23582  erdszelem8  23744  pconcon  23777  cvmlift2lem12  23860  cvmlift3lem2  23866  cvmlift3lem5  23869  cvmlift3lem7  23871  cvmlift3lem8  23872  eupath2  23919  nodenselem5  24410  axeuclidlem  24662  axcontlem2  24665  btwnconn1lem13  24794  ltflcei  24998  lxflflp1  25000  itg2addnclem  25003  itg2addnclem2  25004  itg2gt0cn  25006  bddiblnc  25021  ftc1cnnc  25025  svs3  25591  islimrs3  25684  elicc3  26331  nn0prpwlem  26341  locfincmp  26407  neibastop2lem  26412  sstotbnd2  26601  equivtotbnd  26605  isbndx  26609  ssbnd  26615  heibor1lem  26636  rrncmslem  26659  elrfi  26872  eldioph2  26944  eldioph2b  26945  diophin  26955  diophren  26999  rencldnfilem  27006  irrapxlem2  27011  irrapxlem3  27012  irrapxlem4  27013  irrapxlem5  27014  pellex  27023  pell1234qrne0  27041  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell14qrgt0  27047  pell1234qrdich  27049  pell14qrdich  27057  pell1qrge1  27058  pell1qrgap  27062  pellfundex  27074  congabseq  27164  jm2.26lem3  27197  jm2.27b  27202  jm2.27  27204  fnwe2lem2  27251  kelac1  27264  uvcff  27343  uvcf1  27344  lindfmm  27400  lnrfg  27426  hbt  27437  cntzsdrg  27613  stoweidlem31  27883  constr3cycl  28407  frgra3vlem2  28425  2pthfrgrarn2  28434  islshpat  29829  lfl1dim  29933  lfl1dim2N  29934  lkrpssN  29975  glbconN  30188  hlhgt2  30200  3dim2  30279  3dim3  30280  islln3  30321  islvol5  30390  2lplnja  30430  dalem19  30493  isline4N  30588  2polssN  30726  lhpmatb  30842  4atex  30887  trlatn0  30983  cdlemf2  31373  dialss  31858  diaglbN  31867  diaintclN  31870  dibglbN  31978  dibintclN  31979  dihlsscpre  32046  dihglblem5aN  32104  dihglblem2aN  32105  dihglblem4  32109  dihatexv  32150  dihjat1lem  32240  lcfl6  32312  lcfl8  32314  mapdval2N  32442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator