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  7102  ressress  13205  latjjdir  14210  grprcan  14515  grpsubrcan  14547  grpaddsubass  14555  zntoslem  16510  ipdir  16543  ipass  16549  divstgpopn  17802  grpomuldivass  20916  grpopnpcan2  20920  nvmdi  21208  dmdsl3  22895  btwnconn1lem7  24716  grpodrcan  25375  dblsubvec  25474  mvecrtol2  25477  cvrnbtwn4  29469  paddasslem14  30022  paddasslem17  30025  paddss  30034  pmod1i  30037  cdleme1  30416  cdleme2  30417
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