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

Theorem 3ad2antl3 1161
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 712 . 2  |-  ( ( ( ta  /\  ph )  /\  ch )  ->  th )
323adantl1 1153 1  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  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:  rspc3ev  3173  brcogw  4992  fnsuppresOLD  6113  cocan1  6177  ov6g  6421  dif1en  7787  cfsmolem  8682  coftr  8685  axcc3  8850  axdc4lem  8867  gruf  9219  dedekindle  9779  zdivmul  10976  bpolycl  13997  coprmdvds  14452  lubss  16075  gsumccat  16333  odeq  16898  ghmplusg  17176  lmhmvsca  18011  islindf4  19165  mndifsplit  19430  gsummatr01lem3  19451  gsummatr01  19453  mp2pm2mplem4  19602  elcls  19867  cnpresti  20082  cmpsublem  20192  comppfsc  20325  ptpjcn  20404  elfm3  20743  rnelfmlem  20745  nmoix  21528  caublcls  22039  ig1pdvds  22869  coeid3  22929  amgm  23646  brbtwn2  24625  colinearalg  24630  axsegconlem1  24637  ax5seglem1  24648  ax5seglem2  24649  usgra2edg  24799  clwwlkel  25210  clwwisshclww  25224  homco1  27133  hoadddi  27135  br6  29970  upixp  31502  filbcmb  31513  3dim1  32484  llni  32525  lplni  32549  lvoli  32592  cdleme42mgN  33507  mzprename  35043  infmrgelbi  35175  relexpxpmin  35696  lcmdvds  36062  n0p  36812  fprodle  36972  limcleqr  37018  stoweidlem17  37167  stoweidlem28  37178  fourierdlem12  37269  fourierdlem41  37298  fourierdlem42  37299  fourierdlem74  37331  fourierdlem77  37334
  Copyright terms: Public domain W3C validator