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

Theorem 3ad2antr2 1124
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 698 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1119 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  axdc4lem  8337  ioc0  10965  grpsubadd  14878  zntoslem  16839  trcfilu  18326  constr2wlk  21600  constr2trl  21601  constr3trllem1  21639  grpopnpcan2  21843  mdsl3  23821  dvrcan5  24231  brofs2  26013  brifs2  26014  ftc1anc  26290  frinfm  26439  welb  26440  fdc  26451  unichnidl  26643  swrdccatin2lem1  28228  cvrnbtwn2  30135  islpln2a  30407  paddss1  30676  paddss2  30677  paddasslem17  30695  tendospass  31879
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator