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

Theorem 3ad2antr3 1172
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 720 . 2  |-  ( (
ph  /\  ( ta  /\ 
ch ) )  ->  th )
323adantr1 1164 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  fpr2g  6079  frfi  7764  ressress  15125  funcestrcsetclem9  15971  funcsetcestrclem9  15986  latjjdir  16288  grprcan  16637  grpsubrcan  16673  grpaddsubass  16682  mhmmnd  16746  zntoslem  19064  ipdir  19143  ipass  19149  qustgpopn  21071  constr3trllem1  25315  wwlkextproplem3  25408  grpomuldivass  25914  grpopnpcan2  25918  nvmdi  26208  dmdsl3  27905  dvrcan5  28503  esum2d  28861  voliune  28999  btwnconn1lem7  30804  poimirlem4  31851  cvrnbtwn4  32757  paddasslem14  33310  paddasslem17  33313  paddss  33322  pmod1i  33325  cdleme1  33705  cdleme2  33706  bgoldbst  38692  funcringcsetcALTV2lem9  39637  funcringcsetclem9ALTV  39660
  Copyright terms: Public domain W3C validator