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

Theorem 3ad2antr3 1125
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 698 . 2  |-  ( (
ph  /\  ( ta  /\ 
ch ) )  ->  th )
323adantr1 1117 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  frfi  7354  ressress  13528  latjjdir  14535  grprcan  14840  grpsubrcan  14872  grpaddsubass  14880  zntoslem  16839  ipdir  16872  ipass  16878  divstgpopn  18151  constr3trllem1  21639  grpomuldivass  21839  grpopnpcan2  21843  nvmdi  22133  dmdsl3  23820  dvrcan5  24231  voliune  24587  btwnconn1lem7  26029  cvrnbtwn4  30139  paddasslem14  30692  paddasslem17  30695  paddss  30704  pmod1i  30707  cdleme1  31086  cdleme2  31087
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