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  8081  ioc0  10703  grpsubadd  14553  zntoslem  16510  grpopnpcan2  20920  mdsl3  22896  brofs2  24700  brifs2  24701  grpodlcan  25376  dblsubvec  25474  mvecrtol2  25477  frinfm  26416  welb  26417  fdc  26455  unichnidl  26656  cvrnbtwn2  29465  islpln2a  29737  paddss1  30006  paddss2  30007  paddasslem17  30025  tendospass  31209
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