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

Theorem 3ad2antr3 1164
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 714 . 2  |-  ( (
ph  /\  ( ta  /\ 
ch ) )  ->  th )
323adantr1 1156 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  fpr2g  6112  frfi  7799  ressress  14906  funcestrcsetclem9  15741  funcsetcestrclem9  15756  latjjdir  16058  grprcan  16407  grpsubrcan  16443  grpaddsubass  16452  mhmmnd  16516  zntoslem  18893  ipdir  18972  ipass  18978  qustgpopn  20910  constr3trllem1  25067  wwlkextproplem3  25160  grpomuldivass  25665  grpopnpcan2  25669  nvmdi  25959  dmdsl3  27647  dvrcan5  28236  esum2d  28540  voliune  28678  btwnconn1lem7  30431  cvrnbtwn4  32297  paddasslem14  32850  paddasslem17  32853  paddss  32862  pmod1i  32865  cdleme1  33245  cdleme2  33246  bgoldbst  37832  funcringcsetcALTV2lem9  38363  funcringcsetclem9ALTV  38386
  Copyright terms: Public domain W3C validator