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

Theorem 3ad2antr2 1162
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 715 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr3 1157 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  ta )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  axdc4lem  8847  ioc0  11588  grpsubadd  15998  psrbaglesupp  17887  zntoslem  18464  trcfilu  20665  constr2wlk  24423  constr2trl  24424  constr3trllem1  24473  grpopnpcan2  25078  mdsl3  27058  dvrcan5  27608  brofs2  29654  brifs2  29655  ftc1anc  30025  frinfm  30153  welb  30154  fdc  30165  unichnidl  30355  funcringcsetclem9  32384  ldepsprlem  32555  cvrnbtwn2  34473  islpln2a  34745  paddss1  35014  paddss2  35015  paddasslem17  35033  tendospass  36217
  Copyright terms: Public domain W3C validator