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

Theorem 3ad2antr3 1155
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 1147 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  frfi  7658  ressress  14337  latjjdir  15376  grprcan  15673  grpsubrcan  15709  grpaddsubass  15717  zntoslem  18098  ipdir  18177  ipass  18183  divstgpopn  19806  constr3trllem1  23671  grpomuldivass  23871  grpopnpcan2  23875  nvmdi  24165  dmdsl3  25854  dvrcan5  26395  voliune  26779  btwnconn1lem7  28258  wwlkextproplem3  30700  cvrnbtwn4  33230  paddasslem14  33783  paddasslem17  33786  paddss  33795  pmod1i  33798  cdleme1  34177  cdleme2  34178
  Copyright terms: Public domain W3C validator