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

Theorem 3ad2antl3 1152
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1
Assertion
Ref Expression
3ad2antl3

Proof of Theorem 3ad2antl3
StepHypRef Expression
1 3ad2antl.1 . . 3
21adantll 713 . 2
323adantl1 1144 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 965
This theorem is referenced by:  rspc3ev  3193  brcogw  5125  fnsuppresOLD  6063  cocan1  6120  ov6g  6361  dif1enOLD  7679  dif1en  7680  cfsmolem  8576  coftr  8579  axcc3  8744  axdc4lem  8761  gruf  9115  dedekindle  9671  zdivmul  10852  coprmdvds  13946  lubss  15450  gsumccat  15678  odeq  16214  ghmplusg  16489  lmhmvsca  17302  islindf4  18460  mndifsplit  18710  gsummatr01lem3  18731  gsummatr01  18733  mp2pm2mplem4  18881  elcls  19076  cnpresti  19291  cmpsublem  19401  ptpjcn  19583  elfm3  19922  rnelfmlem  19924  nmoix  20707  ig1pdvds  22048  coeid3  22108  amgm  22784  brbtwn2  23620  colinearalg  23625  axsegconlem1  23632  ax5seglem1  23643  ax5seglem2  23644  usgra2edg  23770  homco1  25674  hoadddi  25676  br6  28023  bpolycl  28651  comppfsc  29039  upixp  29083  filbcmb  29094  mzprename  29546  infmrgelbi  29679  limcleqr  30415  stoweidlem17  30546  stoweidlem28  30557  fourierdlem12  30648  fourierdlem41  30677  fourierdlem42  30678  fourierdlem74  30710  clwwlkel  31332  clwwisshclww  31348  3dim1  33962  llni  34003  lplni  34027  lvoli  34070  cdleme42mgN  34983
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
  Copyright terms: Public domain W3C validator