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

Theorem 3ad2antl3 1137
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 698 . 2
323adantl1 1129 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  /\w3a 950
This theorem is referenced by:  rspc3ev  3061  brcogw  4979  fnsuppresOLD  5907  cocan1  5963  ov6g  6198  dif1enOLD  7503  dif1en  7504  cfsmolem  8386  coftr  8389  axcc3  8554  axdc4lem  8571  gruf  8924  dedekindle  9480  zdivmul  10659  coprmdvds  13728  lubss  15231  gsumccat  15456  odeq  15990  ghmplusg  16264  lmhmvsca  16935  islindf4  17966  mndifsplit  18146  gsummatr01lem3  18167  gsummatr01  18169  elcls  18381  cnpresti  18596  cmpsublem  18706  ptpjcn  18888  elfm3  19227  rnelfmlem  19229  nmoix  20008  ig1pdvds  21389  coeid3  21449  amgm  22125  brbtwn2  22830  colinearalg  22835  axsegconlem1  22842  ax5seglem1  22853  ax5seglem2  22854  usgra2edg  22980  homco1  24884  hoadddi  24886  br6  27269  bpolycl  27897  comppfsc  28250  upixp  28294  filbcmb  28305  mzprename  28759  infmrgelbi  28892  stoweidlem17  29486  stoweidlem28  29497  clwwlkel  30129  clwwisshclww  30145  3dim1  32548  llni  32589  lplni  32613  lvoli  32656  cdleme42mgN  33569
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 179  df-an 364  df-3an 952
  Copyright terms: Public domain W3C validator