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

Theorem 3adant3r3 1165
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 1155 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1119 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  ressress  13528  plttr  14429  plelttr  14431  joinle  14452  meetle  14459  latjle12  14493  latlem12  14509  latledi  14520  latmlej11  14521  latmlej21  14523  latmlej22  14524  latjass  14526  latj12  14527  latj31  14530  ipopos  14588  latdisdlem  14617  ismndd  14721  imasmnd2  14734  imasmnd  14735  grpaddsubass  14880  grpsubsub4  14883  grpnpncan  14885  imasgrp2  14935  imasgrp  14936  frgp0  15394  cmn12  15434  abladdsub  15441  imasrng  15727  dvrass  15797  lss1  16017  islmhm2  16116  psrgrp  16464  psrlmod  16467  zntoslem  16839  ipdir  16872  t1sep  17436  mettri2  18373  xmetrtri  18387  xmetrtri2  18388  pi1grplem  19076  dchrabl  21040  grpomuldivass  21839  grpopnpcan2  21843  grponpncan  21845  grpodiveq  21846  ablomuldiv  21879  ablodivdiv4  21881  nvadd12  22104  nvmdi  22133  nvsubadd  22138  nvmtri2  22163  dipdi  22346  dipsubdir  22351  dipsubdi  22352  ax5seglem4  25873  cgr3tr4  25988  cgr3rflx  25990  seglemin  26049  linerflx1  26085  elicc3  26322  rngosubdi  26571  rngosubdir  26572  igenval2  26678  dmncan1  26688  mendlmod  27480  latmassOLD  30089  omlfh1N  30118  omlfh3N  30119  cvrnbtwn  30131  cvrnbtwn2  30135  cvrnbtwn4  30139  hlatj12  30230  cvrntr  30284  islpln2a  30407  3atnelvolN  30445  elpadd2at2  30666  paddasslem17  30695  paddass  30697  paddssw2  30703  pmapjlln1  30714  ltrn2ateq  31039  cdlemc3  31052  cdleme1b  31085  cdleme3b  31088  cdleme3c  31089  cdleme9b  31111  erngdvlem3  31849  erngdvlem3-rN  31857  dvalveclem  31885
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator