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

Theorem 3adant3r2 1163
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 1154 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1117 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  plttr  14427  latjlej2  14495  latmlem1  14510  latmlem2  14511  latledi  14518  latmlej11  14519  latmlej12  14520  ipopos  14586  grppnpcan2  14882  mulgsubdir  14921  imasrng  15725  zntoslem  16837  mettri2  18371  mettri  18382  xmetrtri  18385  xmetrtri2  18386  metrtri  18387  grpopnpcan2  21841  grponnncan2  21842  ablomuldiv  21877  ablonnncan1  21883  nvmdi  22131  dipdi  22344  dipassr  22347  dipsubdir  22349  dipsubdi  22350  btwncomim  25947  cgr3tr4  25986  cgr3rflx  25988  colinbtwnle  26052  rngosubdi  26569  rngosubdir  26570  dmncan1  26686  dmncan2  26687  mendlmod  27478  omlfh1N  30056  omlfh3N  30057  cvrnbtwn3  30074  cvrnbtwn4  30077  cvrcmp2  30082  hlatjrot  30170  cvrat3  30239  lplnribN  30348  ltrn2ateq  30977  dvalveclem  31823
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator