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

Theorem 3adant3r2 1162
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 1153 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1116 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  plttr  14314  latjlej2  14382  latmlem1  14397  latmlem2  14398  latledi  14405  latmlej11  14406  latmlej12  14407  ipopos  14473  grppnpcan2  14769  mulgsubdir  14808  imasrng  15612  zntoslem  16727  mettri2  18119  mettri  18129  xmetrtri  18132  xmetrtri2  18133  metrtri  18134  grpopnpcan2  21352  grponnncan2  21353  ablomuldiv  21388  ablonnncan1  21394  nvmdi  21642  dipdi  21855  dipassr  21858  dipsubdir  21860  dipsubdi  21861  btwncomim  25463  cgr3tr4  25502  cgr3rflx  25504  colinbtwnle  25568  rngosubdi  26175  rngosubdir  26176  dmncan1  26292  dmncan2  26293  mendlmod  27092  omlfh1N  29507  omlfh3N  29508  cvrnbtwn3  29525  cvrnbtwn4  29528  cvrcmp2  29533  hlatjrot  29621  cvrat3  29690  lplnribN  29799  ltrn2ateq  30428  dvalveclem  31274
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 937
  Copyright terms: Public domain W3C validator