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  13221  plttr  14120  plelttr  14122  joinle  14143  meetle  14150  latjle12  14184  latlem12  14200  latledi  14211  latmlej11  14212  latmlej21  14214  latmlej22  14215  latjass  14217  latj12  14218  latj31  14221  ipopos  14279  latdisdlem  14308  ismndd  14412  imasmnd2  14425  imasmnd  14426  grpaddsubass  14571  grpsubsub4  14574  grpnpncan  14576  imasgrp2  14626  imasgrp  14627  frgp0  15085  cmn12  15125  abladdsub  15132  imasrng  15418  dvrass  15488  lss1  15712  islmhm2  15811  psrgrp  16159  psrlmod  16162  zntoslem  16526  ipdir  16559  t1sep  17114  mettri2  17922  xmetrtri  17935  xmetrtri2  17936  pi1grplem  18563  dchrabl  20509  grpomuldivass  20932  grpopnpcan2  20936  grponpncan  20938  grpodiveq  20939  ablomuldiv  20972  ablodivdiv4  20974  nvadd12  21195  nvmdi  21224  nvsubadd  21229  nvmtri2  21254  dipdi  21437  dipsubdir  21442  dipsubdi  21443  ax5seglem4  24632  cgr3tr4  24747  cgr3rflx  24749  seglemin  24808  linerflx1  24844  addassv  25759  subaddv  25774  tcnvec  25793  homgrf  25905  elicc3  26331  rngosubdi  26687  rngosubdir  26688  igenval2  26794  dmncan1  26804  mendlmod  27604  latmassOLD  30041  omlfh1N  30070  omlfh3N  30071  cvrnbtwn  30083  cvrnbtwn2  30087  cvrnbtwn4  30091  hlatj12  30182  cvrntr  30236  islpln2a  30359  3atnelvolN  30397  elpadd2at2  30618  paddasslem17  30647  paddass  30649  paddssw2  30655  pmapjlln1  30666  ltrn2ateq  30991  cdlemc3  31004  cdleme1b  31037  cdleme3b  31040  cdleme3c  31041  cdleme9b  31063  erngdvlem3  31801  erngdvlem3-rN  31809  dvalveclem  31837
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