Theorem 3ad2antl3 1186

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpl3  1192  simpl3l  1227  simpl3r  1228  simpl31  1253  simpl32  1254  simpl33  1255  rspc3ev  3575  brcogw  5780  cocan1  7172  ov6g  7445  fpr1  8128  dif1enALT  9059  cfsmolem  10035  coftr  10038  axcc3  10203  axdc4lem  10220  gruf  10576  dedekindle  11148  zdivmul  12401  cshf1  14532  cshimadifsn  14551  fprodle  15715  bpolycl  15771  lcmdvds  16322  lubss  18240  gsumccatOLD  18488  odeq  19167  ghmplusg  19456  lmhmvsca  20316  islindf4  21054  mndifsplit  21794  gsummatr01lem3  21815  gsummatr01  21817  mp2pm2mplem4  21967  elcls  22233  cnpresti  22448  cmpsublem  22559  comppfsc  22692  ptpjcn  22771  elfm3  23110  rnelfmlem  23112  nmoix  23902  caublcls  24482  ig1pdvds  25350  coeid3  25410  amgm  26149  brbtwn2  27282  colinearalg  27287  axsegconlem1  27294  ax5seglem1  27305  ax5seglem2  27306  homco1  30172  hoadddi  30174  br6  33733  lindsenlbs  35781  upixp  35896  filbcmb  35907  3dim1  37488  llni  37529  lplni  37553  lvoli  37596  cdleme42mgN  38509  mzprename  40578  infmrgelbi  40707  relexpxpmin  41332  n0p  42598  rexabslelem  42965  limcleqr  43192  fnlimfvre  43222  stoweidlem17  43565  stoweidlem28  43576  fourierdlem12  43667  fourierdlem41  43696  fourierdlem42  43697  fourierdlem74  43728  fourierdlem77  43731  qndenserrnopnlem  43845  issalnnd  43891  hspmbllem2  44172  issmfle  44290  smflimlem2  44317  smflimmpt  44354  smfinflem  44361  smflimsuplem7  44370  smflimsupmpt  44373  smfliminfmpt  44376  lighneallem3  45070