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

Theorem 3ad2antr3 1122
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 696 . 2  |-  ( (
ph  /\  ( ta  /\ 
ch ) )  ->  th )
323adantr1 1114 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  frfi  7118  ressress  13221  latjjdir  14226  grprcan  14531  grpsubrcan  14563  grpaddsubass  14571  zntoslem  16526  ipdir  16559  ipass  16565  divstgpopn  17818  grpomuldivass  20932  grpopnpcan2  20936  nvmdi  21224  dmdsl3  22911  btwnconn1lem7  24788  grpodrcan  25478  dblsubvec  25577  mvecrtol2  25580  constr3trllem1  28396  cvrnbtwn4  30091  paddasslem14  30644  paddasslem17  30647  paddss  30656  pmod1i  30659  cdleme1  31038  cdleme2  31039
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator