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

Theorem 3ad2antr2 1121
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antr2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )

Proof of Theorem 3ad2antr2
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantrl 696 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1116 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:  axdc4lem  8097  ioc0  10719  grpsubadd  14569  zntoslem  16526  grpopnpcan2  20936  mdsl3  22912  brofs2  24772  brifs2  24773  grpodlcan  25479  dblsubvec  25577  mvecrtol2  25580  frinfm  26519  welb  26520  fdc  26558  unichnidl  26759  constr3trllem1  28396  cvrnbtwn2  30087  islpln2a  30359  paddss1  30628  paddss2  30629  paddasslem17  30647  tendospass  31831
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