Theorem 3ad2antl3 1218

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 746	. 2 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1210	1 ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  rspc3ev  3297  brcogw  5212  cocan1  6446  ov6g  6696  dif1en  8078  cfsmolem  8975  coftr  8978  axcc3  9143  axdc4lem  9160  gruf  9512  dedekindle  10080  zdivmul  11325  cshimadifsn  13426  fprodle  14566  bpolycl  14622  lcmdvds  15159  coprmdvdsOLD  15205  lubss  16944  gsumccat  17201  odeq  17792  ghmplusg  18072  lmhmvsca  18866  islindf4  19996  mndifsplit  20261  gsummatr01lem3  20282  gsummatr01  20284  mp2pm2mplem4  20433  elcls  20687  cnpresti  20902  cmpsublem  21012  comppfsc  21145  ptpjcn  21224  elfm3  21564  rnelfmlem  21566  nmoix  22343  caublcls  22915  ig1pdvds  23740  coeid3  23800  amgm  24517  brbtwn2  25585  colinearalg  25590  axsegconlem1  25597  ax5seglem1  25608  ax5seglem2  25609  usgra2edg  25911  clwwlkel  26321  clwwisshclww  26335  homco1  28044  hoadddi  28046  br6  30900  lindsenlbs  32574  upixp  32694  filbcmb  32705  3dim1  33771  llni  33812  lplni  33836  lvoli  33879  cdleme42mgN  34794  mzprename  36330  infmrgelbi  36460  relexpxpmin  37028  n0p  38234  limcleqr  38711  fnlimfvre  38741  stoweidlem17  38910  stoweidlem28  38921  fourierdlem12  39012  fourierdlem41  39041  fourierdlem42  39042  fourierdlem74  39073  fourierdlem77  39076  qndenserrnopnlem  39193  issalnnd  39239  hspmbllem2  39517  issmfle  39632  smflimlem2  39658  lighneallem3  40062  edginwlk  40839