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

Theorem ad3antrrr 710
Description: Deduction adding 3 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  6642  oaabs2  6643  omabs  6645  undom  6950  sbthlem8  6978  findcard3  7100  marypha1lem  7186  cantnfle  7372  cantnfp1  7383  cantnflem1c  7389  sornom  7903  enfin2i  7947  ttukeylem6  8141  fpwwe2lem13  8264  fpwwe2  8265  winalim2  8318  wuncval2  8369  xlemul1a  10608  difreicc  10767  faclbnd  11303  ello12  11990  lo1bdd2  11998  elo12  12001  rlimclim1  12019  rlimcld2  12052  o1co  12060  o1of2  12086  o1rlimmul  12092  rlimsqzlem  12122  isercoll  12141  o1fsum  12271  supcvg  12314  dvds2ln  12559  isprm5  12791  pcadd  12937  vdwlem2  13029  vdwlem11  13038  prdsval  13355  mreexexlem4d  13549  isacs2  13555  catcocl  13587  catass  13588  catpropd  13612  subccocl  13719  fullsubc  13724  funcco  13745  funcpropd  13774  fullpropd  13794  ffthiso  13803  isnat  13821  natpropd  13850  fucpropd  13851  xpcval  13951  evlf2  13992  curfpropd  14007  curfuncf  14012  uncfcurf  14013  curf2ndf  14021  hofcl  14033  hofpropd  14041  yonffthlem  14056  drsdirfi  14072  isacs3lem  14269  acsfiindd  14280  resmhm2b  14438  conjnmzb  14717  pgpfi  14916  sylow3lem2  14939  efgredlem  15056  frgpnabllem1  15161  dprdfcntz  15250  ablfac1b  15305  pgpfac1lem3  15312  pgpfac1lem5  15314  pgpfaclem3  15318  islmhm2  15795  lspsneleq  15868  psrval  16110  psrass1  16150  resspsrmul  16161  mplbas2  16212  coe1tmmul  16353  znunit  16517  ordtrest2lem  16933  cnpnei  16993  iscncl  16998  cncls  17003  cnntr  17004  cncnp  17009  lmcnp  17032  isreg2  17105  hauscmplem  17133  cmpfi  17135  1stcfb  17171  1stcrest  17179  2ndcctbss  17181  2ndcomap  17184  islly2  17210  cldllycmp  17221  lly1stc  17222  llycmpkgen2  17245  1stckgenlem  17248  kgencn2  17252  kgencn3  17253  ptbasfi  17276  ptpjopn  17306  xkoccn  17313  txdis1cn  17329  txlly  17330  txnlly  17331  txtube  17334  txcmplem2  17336  tx1stc  17344  txkgen  17346  xkopt  17349  xkoco2cn  17352  xkococnlem  17353  xkococn  17354  xkoinjcn  17381  tgqtop  17403  regr1lem  17430  kqreglem1  17432  nrmhmph  17485  rnelfmlem  17647  rnelfm  17648  fmfnfmlem4  17652  fmfnfm  17653  ufldom  17657  flimopn  17670  hauspwpwf1  17682  fclsopn  17709  fclsnei  17714  fclsrest  17719  alexsublem  17738  alexsubALTlem3  17743  ptcmplem2  17747  ptcmplem3  17748  symgtgp  17784  tgpt0  17801  divstgpopn  17802  divstgplem  17803  tsmsxplem1  17835  met1stc  18067  met2ndci  18068  prdsxmslem2  18075  metcnp3  18086  nmoleub  18240  reconnlem2  18332  xrge0tsms  18339  cncfco  18411  cnheibor  18453  lebnumlem3  18461  lebnum  18462  nmoleub2lem2  18597  nmoleub3  18600  iscfil2  18692  iscau4  18705  iscmet3lem2  18718  equivcfil  18725  equivcau  18726  caubl  18733  ovolshftlem2  18869  ovolicc2lem4  18879  uniioombl  18944  i1fmulclem  19057  mbfi1fseqlem6  19075  itg2const2  19096  itg2split  19104  ellimc2  19227  ellimc3  19229  limcflf  19231  dvmptfsum  19322  dvferm1  19332  dvferm2  19334  dvlip2  19342  c1lip1  19344  lhop1  19361  ftc1a  19384  ply1divex  19522  plyeq0lem  19592  plymullem1  19596  coemullem  19631  coemulc  19636  ulmshftlem  19768  ulmcaulem  19771  ulmcau  19772  ulmbdd  19775  ulmcn  19776  ulmdvlem3  19779  pserulm  19798  pserdvlem2  19804  abelthlem8  19815  xrlimcnp  20263  jensen  20283  logfac2  20456  dchrelbas3  20477  dchrpt  20506  lgsquad3  20600  2sqb  20617  rpvmasumlem  20636  dchrisumlem1  20638  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem2  20647  dchrisum0flblem1  20657  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0  20669  mulog2sumlem2  20684  pntlem3  20758  ostth3  20787  isgrp2d  20902  ubthlem3  21451  chirredlem1  22970  chirredlem3  22972  cdj1i  23013  lmdvg  23376  gsumpropd2lem  23379  xrge0tsmsd  23382  esumcst  23436  esumpcvgval  23446  imambfm  23567  erdszelem8  23729  pconcon  23762  cvmlift2lem12  23845  cvmlift3lem2  23851  cvmlift3lem5  23854  cvmlift3lem7  23856  cvmlift3lem8  23857  eupath2  23904  nodenselem5  24339  axeuclidlem  24590  axcontlem2  24593  btwnconn1lem13  24722  svs3  25488  islimrs3  25581  elicc3  26228  nn0prpwlem  26238  locfincmp  26304  neibastop2lem  26309  sstotbnd2  26498  equivtotbnd  26502  isbndx  26506  ssbnd  26512  heibor1lem  26533  rrncmslem  26556  elrfi  26769  eldioph2  26841  eldioph2b  26842  diophin  26852  diophren  26896  rencldnfilem  26903  irrapxlem2  26908  irrapxlem3  26909  irrapxlem4  26910  irrapxlem5  26911  pellex  26920  pell1234qrne0  26938  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell14qrgt0  26944  pell1234qrdich  26946  pell14qrdich  26954  pell1qrge1  26955  pell1qrgap  26959  pellfundex  26971  congabseq  27061  jm2.26lem3  27094  jm2.27b  27099  jm2.27  27101  fnwe2lem2  27148  kelac1  27161  uvcff  27240  uvcf1  27241  lindfmm  27297  lnrfg  27323  hbt  27334  cntzsdrg  27510  stoweidlem31  27780  frgra3vlem2  28179  islshpat  29207  lfl1dim  29311  lfl1dim2N  29312  lkrpssN  29353  glbconN  29566  hlhgt2  29578  3dim2  29657  3dim3  29658  islln3  29699  islvol5  29768  2lplnja  29808  dalem19  29871  isline4N  29966  2polssN  30104  lhpmatb  30220  4atex  30265  trlatn0  30361  cdlemf2  30751  dialss  31236  diaglbN  31245  diaintclN  31248  dibglbN  31356  dibintclN  31357  dihlsscpre  31424  dihglblem5aN  31482  dihglblem2aN  31483  dihglblem4  31487  dihatexv  31528  dihjat1lem  31618  lcfl6  31690  lcfl8  31692  mapdval2N  31820
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