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

Theorem 3adant3r2 1215
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 1206 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1165 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  plttr  16168  latjlej2  16264  latmlem1  16279  latmlem2  16280  latledi  16287  latmlej11  16288  latmlej12  16289  ipopos  16358  grppnpcan2  16700  mulgsubdir  16741  imasring  17788  zntoslem  19064  mettri2  21293  mettri  21304  xmetrtri  21307  xmetrtri2  21308  metrtri  21309  grpopnpcan2  25867  grponnncan2  25868  ablomuldiv  25903  ablonnncan1  25909  nvmdi  26157  dipdi  26370  dipassr  26373  dipsubdir  26375  dipsubdi  26376  btwncomim  30606  cgr3tr4  30645  cgr3rflx  30647  colinbtwnle  30711  rngosubdi  31940  rngosubdir  31941  dmncan1  32057  dmncan2  32058  omlfh1N  32577  omlfh3N  32578  cvrnbtwn3  32595  cvrnbtwn4  32598  cvrcmp2  32603  hlatjrot  32691  cvrat3  32760  lplnribN  32869  ltrn2ateq  33499  dvalveclem  34346  mendlmod  35806
  Copyright terms: Public domain W3C validator