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

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

Proof of Theorem 3ad2antr3
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantrl 715 . 2  |-  ( (
ph  /\  ( ta  /\ 
ch ) )  ->  th )
323adantr1 1155 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  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:  frfi  7761  ressress  14548  latjjdir  15587  grprcan  15884  grpsubrcan  15920  grpaddsubass  15929  zntoslem  18362  ipdir  18441  ipass  18447  divstgpopn  20353  constr3trllem1  24326  wwlkextproplem3  24419  grpomuldivass  24927  grpopnpcan2  24931  nvmdi  25221  dmdsl3  26910  dvrcan5  27446  voliune  27841  btwnconn1lem7  29320  cvrnbtwn4  34076  paddasslem14  34629  paddasslem17  34632  paddss  34641  pmod1i  34644  cdleme1  35023  cdleme2  35024
  Copyright terms: Public domain W3C validator