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

Theorem 3ad2antl3 1155
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl3  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl3
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantll 713 . 2  |-  ( ( ( ta  /\  ph )  /\  ch )  ->  th )
323adantl1 1147 1  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  rspc3ev  3220  brcogw  5162  fnsuppresOLD  6112  cocan1  6173  ov6g  6415  dif1enOLD  7741  dif1en  7742  cfsmolem  8639  coftr  8642  axcc3  8807  axdc4lem  8824  gruf  9178  dedekindle  9733  zdivmul  10922  coprmdvds  14091  lubss  15597  gsumccat  15825  odeq  16363  ghmplusg  16638  lmhmvsca  17467  islindf4  18633  mndifsplit  18898  gsummatr01lem3  18919  gsummatr01  18921  mp2pm2mplem4  19070  elcls  19333  cnpresti  19548  cmpsublem  19658  ptpjcn  19840  elfm3  20179  rnelfmlem  20181  nmoix  20964  ig1pdvds  22305  coeid3  22365  amgm  23041  brbtwn2  23877  colinearalg  23882  axsegconlem1  23889  ax5seglem1  23900  ax5seglem2  23901  usgra2edg  24044  clwwlkel  24455  clwwisshclww  24469  homco1  26382  hoadddi  26384  br6  28749  bpolycl  29377  comppfsc  29766  upixp  29810  filbcmb  29821  mzprename  30273  infmrgelbi  30405  limcleqr  31141  stoweidlem17  31272  stoweidlem28  31283  fourierdlem12  31374  fourierdlem41  31403  fourierdlem42  31404  fourierdlem74  31436  3dim1  34138  llni  34179  lplni  34203  lvoli  34246  cdleme42mgN  35159
  Copyright terms: Public domain W3C validator