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

Theorem 3adantr3 1116
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
3adantr.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
3adantr3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )

Proof of Theorem 3adantr3
StepHypRef Expression
1 3simpa 952 . 2  |-  ( ( ps  /\  ch  /\  ta )  ->  ( ps 
/\  ch ) )
2 3adantr.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ad2antr1  1120  3ad2antr2  1121  3adant3r3  1162  sotr2  4359  dfwe2  4589  smogt  6400  wlogle  9322  tanadd  12463  prdsmndd  14421  imasrng  15418  prdslmodd  15742  mpllsslem  16196  ptclsg  17325  tmdgsum2  17795  isxmet2d  17908  xmetres2  17941  prdsxmetlem  17948  comet  18075  iimulcl  18451  icoopnst  18453  iocopnst  18454  icccvx  18464  dvfsumrlim  19394  dvfsumrlim2  19395  grponpncan  20938  nvsubadd  21229  dmdsl3  22911  rescon  23792  dblsubvec  25577  fzadd2  26547  isdrngo2  26692  iscringd  26727  unichnidl  26759  lplnle  30351  2llnjN  30378  2lplnj  30431  osumcllem11N  30777  cdleme1  31038  erngplus2  31615  erngplus2-rN  31623  erngdvlem3  31801  erngdvlem3-rN  31809  dvaplusgv  31821  dvalveclem  31837  dvhvaddass  31909  dvhlveclem  31920  dihmeetlem12N  32130
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 936
  Copyright terms: Public domain W3C validator