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

Theorem 3adant3r3 1162
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant3r3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )

Proof of Theorem 3adant3r3
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1152 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1116 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ressress  13205  plttr  14104  plelttr  14106  joinle  14127  meetle  14134  latjle12  14168  latlem12  14184  latledi  14195  latmlej11  14196  latmlej21  14198  latmlej22  14199  latjass  14201  latj12  14202  latj31  14205  ipopos  14263  latdisdlem  14292  ismndd  14396  imasmnd2  14409  imasmnd  14410  grpaddsubass  14555  grpsubsub4  14558  grpnpncan  14560  imasgrp2  14610  imasgrp  14611  frgp0  15069  cmn12  15109  abladdsub  15116  imasrng  15402  dvrass  15472  lss1  15696  islmhm2  15795  psrgrp  16143  psrlmod  16146  zntoslem  16510  ipdir  16543  t1sep  17098  mettri2  17906  xmetrtri  17919  xmetrtri2  17920  pi1grplem  18547  dchrabl  20493  grpomuldivass  20916  grpopnpcan2  20920  grponpncan  20922  grpodiveq  20923  ablomuldiv  20956  ablodivdiv4  20958  nvadd12  21179  nvmdi  21208  nvsubadd  21213  nvmtri2  21238  dipdi  21421  dipsubdir  21426  dipsubdi  21427  ax5seglem4  24560  cgr3tr4  24675  cgr3rflx  24677  seglemin  24736  linerflx1  24772  addassv  25656  subaddv  25671  tcnvec  25690  homgrf  25802  elicc3  26228  rngosubdi  26584  rngosubdir  26585  igenval2  26691  dmncan1  26701  mendlmod  27501  latmassOLD  29419  omlfh1N  29448  omlfh3N  29449  cvrnbtwn  29461  cvrnbtwn2  29465  cvrnbtwn4  29469  hlatj12  29560  cvrntr  29614  islpln2a  29737  3atnelvolN  29775  elpadd2at2  29996  paddasslem17  30025  paddass  30027  paddssw2  30033  pmapjlln1  30044  ltrn2ateq  30369  cdlemc3  30382  cdleme1b  30415  cdleme3b  30418  cdleme3c  30419  cdleme9b  30441  erngdvlem3  31179  erngdvlem3-rN  31187  dvalveclem  31215
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  df-3an 936
  Copyright terms: Public domain W3C validator