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

Theorem 3adant3r2 1197
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 1188 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1148 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  plttr  15161  latjlej2  15257  latmlem1  15272  latmlem2  15273  latledi  15280  latmlej11  15281  latmlej12  15282  ipopos  15351  grppnpcan2  15640  mulgsubdir  15679  imasrng  16733  zntoslem  18011  mettri2  19938  mettri  19949  xmetrtri  19952  xmetrtri2  19953  metrtri  19954  grpopnpcan2  23762  grponnncan2  23763  ablomuldiv  23798  ablonnncan1  23804  nvmdi  24052  dipdi  24265  dipassr  24268  dipsubdir  24270  dipsubdi  24271  btwncomim  28066  cgr3tr4  28105  cgr3rflx  28107  colinbtwnle  28171  rngosubdi  28785  rngosubdir  28786  dmncan1  28902  dmncan2  28903  mendlmod  29576  omlfh1N  32999  omlfh3N  33000  cvrnbtwn3  33017  cvrnbtwn4  33020  cvrcmp2  33025  hlatjrot  33113  cvrat3  33182  lplnribN  33291  ltrn2ateq  33920  dvalveclem  34766
  Copyright terms: Public domain W3C validator