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

Theorem 3adant3r2 1164
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 1155 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1118 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  plttr  14458  latjlej2  14526  latmlem1  14541  latmlem2  14542  latledi  14549  latmlej11  14550  latmlej12  14551  ipopos  14617  grppnpcan2  14913  mulgsubdir  14952  imasrng  15756  zntoslem  16868  mettri2  18402  mettri  18413  xmetrtri  18416  xmetrtri2  18417  metrtri  18418  grpopnpcan2  21872  grponnncan2  21873  ablomuldiv  21908  ablonnncan1  21914  nvmdi  22162  dipdi  22375  dipassr  22378  dipsubdir  22380  dipsubdi  22381  btwncomim  25978  cgr3tr4  26017  cgr3rflx  26019  colinbtwnle  26083  rngosubdi  26607  rngosubdir  26608  dmncan1  26724  dmncan2  26725  mendlmod  27516  omlfh1N  30154  omlfh3N  30155  cvrnbtwn3  30172  cvrnbtwn4  30175  cvrcmp2  30180  hlatjrot  30268  cvrat3  30337  lplnribN  30446  ltrn2ateq  31075  dvalveclem  31921
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator