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

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

Proof of Theorem 3adant3r2
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1152 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1115 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  plttr  14120  latjlej2  14188  latmlem1  14203  latmlem2  14204  latledi  14211  latmlej11  14212  latmlej12  14213  ipopos  14279  grppnpcan2  14575  mulgsubdir  14614  imasrng  15418  zntoslem  16526  mettri2  17922  mettri  17932  xmetrtri  17935  xmetrtri2  17936  metrtri  17937  grpopnpcan2  20936  grponnncan2  20937  ablomuldiv  20972  ablonnncan1  20978  nvmdi  21224  dipdi  21437  dipassr  21440  dipsubdir  21442  dipsubdi  21443  btwncomim  24708  cgr3tr4  24747  cgr3rflx  24749  colinbtwnle  24813  grpodrcan  25478  homgrf  25905  rngosubdi  26687  rngosubdir  26688  dmncan1  26804  dmncan2  26805  mendlmod  27604  omlfh1N  30070  omlfh3N  30071  cvrnbtwn3  30088  cvrnbtwn4  30091  cvrcmp2  30096  hlatjrot  30184  cvrat3  30253  lplnribN  30362  ltrn2ateq  30991  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