Theorem 3ad2antl3 1168

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1069

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 199  df-an 388  df-3an 1071

This theorem is referenced by:  simpl3  1174  simpl3l  1209  simpl3r  1210  simpl31  1235  simpl32  1236  simpl33  1237  rspc3ev  3545  brcogw  5585  cocan1  6870  ov6g  7126  dif1en  8544  cfsmolem  9488  coftr  9491  axcc3  9656  axdc4lem  9673  gruf  10029  dedekindle  10602  zdivmul  11865  cshf1  14032  cshimadifsn  14051  fprodle  15208  bpolycl  15264  lcmdvds  15806  lubss  17601  gsumccat  17858  odeq  18452  ghmplusg  18734  lmhmvsca  19551  islindf4  20699  mndifsplit  20964  gsummatr01lem3  20985  gsummatr01  20987  mp2pm2mplem4  21136  elcls  21400  cnpresti  21615  cmpsublem  21726  comppfsc  21859  ptpjcn  21938  elfm3  22277  rnelfmlem  22279  nmoix  23056  caublcls  23630  ig1pdvds  24488  coeid3  24548  amgm  25285  brbtwn2  26409  colinearalg  26414  axsegconlem1  26421  ax5seglem1  26432  ax5seglem2  26433  homco1  29374  hoadddi  29376  br6  32550  fpr1  32697  lindsenlbs  34365  upixp  34483  filbcmb  34494  3dim1  36085  llni  36126  lplni  36150  lvoli  36193  cdleme42mgN  37106  mzprename  38779  infmrgelbi  38909  relexpxpmin  39463  n0p  40762  rexabslelem  41157  limcleqr  41390  fnlimfvre  41420  stoweidlem17  41767  stoweidlem28  41778  fourierdlem12  41869  fourierdlem41  41898  fourierdlem42  41899  fourierdlem74  41930  fourierdlem77  41933  qndenserrnopnlem  42047  issalnnd  42093  hspmbllem2  42374  issmfle  42487  smflimlem2  42513  smflimmpt  42549  smfinflem  42556  smflimsuplem7  42565  smflimsupmpt  42568  smfliminfmpt  42571  lighneallem3  43174