Theorem 3ad2antl3 1160

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

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3
2	1	adantll 713	. 2
3	2	3adantl1 1152	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  rspc3ev  3223  brcogw  5176  fnsuppresOLD  6131  cocan1  6194  ov6g  6440  dif1enOLD  7772  dif1en  7773  cfsmolem  8671  coftr  8674  axcc3  8839  axdc4lem  8856  gruf  9210  dedekindle  9766  zdivmul  10960  coprmdvds  14243  lubss  15751  gsumccat  16009  odeq  16574  ghmplusg  16852  lmhmvsca  17691  islindf4  18873  mndifsplit  19138  gsummatr01lem3  19159  gsummatr01  19161  mp2pm2mplem4  19310  elcls  19574  cnpresti  19789  cmpsublem  19899  comppfsc  20033  ptpjcn  20112  elfm3  20451  rnelfmlem  20453  nmoix  21236  caublcls  21747  ig1pdvds  22577  coeid3  22637  amgm  23320  brbtwn2  24208  colinearalg  24213  axsegconlem1  24220  ax5seglem1  24231  ax5seglem2  24232  usgra2edg  24382  clwwlkel  24793  clwwisshclww  24807  homco1  26720  hoadddi  26722  br6  29186  bpolycl  29814  upixp  30220  filbcmb  30231  mzprename  30682  infmrgelbi  30814  lcmdvds  31214  n0p  31437  fprodle  31604  limcleqr  31650  stoweidlem17  31799  stoweidlem28  31810  fourierdlem12  31901  fourierdlem41  31930  fourierdlem42  31931  fourierdlem74  31963  fourierdlem77  31966  3dim1  35191  llni  35232  lplni  35256  lvoli  35299  cdleme42mgN  36214

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 975