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

Theorem 3ad2antl3 1152
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 1144 1  |-  ( ( ( ps  /\  ta  /\ 
ph )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  rspc3ev  3083  brcogw  5008  fnsuppresOLD  5938  cocan1  5995  ov6g  6228  dif1enOLD  7544  dif1en  7545  cfsmolem  8439  coftr  8442  axcc3  8607  axdc4lem  8624  gruf  8978  dedekindle  9534  zdivmul  10714  coprmdvds  13788  lubss  15291  gsumccat  15519  odeq  16053  ghmplusg  16328  lmhmvsca  17126  islindf4  18267  mndifsplit  18442  gsummatr01lem3  18463  gsummatr01  18465  elcls  18677  cnpresti  18892  cmpsublem  19002  ptpjcn  19184  elfm3  19523  rnelfmlem  19525  nmoix  20308  ig1pdvds  21648  coeid3  21708  amgm  22384  brbtwn2  23151  colinearalg  23156  axsegconlem1  23163  ax5seglem1  23174  ax5seglem2  23175  usgra2edg  23301  homco1  25205  hoadddi  25207  br6  27567  bpolycl  28195  comppfsc  28579  upixp  28623  filbcmb  28634  mzprename  29086  infmrgelbi  29219  stoweidlem17  29812  stoweidlem28  29823  clwwlkel  30455  clwwisshclww  30471  mp2pm2mplem4  30919  3dim1  33111  llni  33152  lplni  33176  lvoli  33219  cdleme42mgN  34132
  Copyright terms: Public domain W3C validator