Theorem 3ad2antl3 1188

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpl3  1194  simpl3l  1229  simpl3r  1230  simpl31  1255  simpl32  1256  simpl33  1257  rspc3ev  3594  brcogw  5811  cocan1  7228  ov6g  7513  fpr1  8236  dif1enlem  9073  dif1ennnALT  9166  cfsmolem  10164  coftr  10167  axcc3  10332  axdc4lem  10349  gruf  10705  dedekindle  11280  zdivmul  12548  cshf1  14716  cshimadifsn  14736  fprodle  15903  bpolycl  15959  lcmdvds  16519  lubss  18419  odeq  19429  ghmplusg  19725  lmhmvsca  20949  islindf4  21745  mndifsplit  22521  gsummatr01lem3  22542  gsummatr01  22544  mp2pm2mplem4  22694  elcls  22958  cnpresti  23173  cmpsublem  23284  comppfsc  23417  ptpjcn  23496  elfm3  23835  rnelfmlem  23837  nmoix  24615  caublcls  25207  ig1pdvds  26083  coeid3  26143  amgm  26899  brbtwn2  28850  colinearalg  28855  axsegconlem1  28862  ax5seglem1  28873  ax5seglem2  28874  homco1  31745  hoadddi  31747  br6  35740  lindsenlbs  37605  upixp  37719  filbcmb  37730  3dim1  39456  llni  39497  lplni  39521  lvoli  39564  cdleme42mgN  40477  mzprename  42732  infmrgelbi  42861  relexpxpmin  43700  n0p  45033  rexabslelem  45407  pimxrneun  45477  limcleqr  45635  fnlimfvre  45665  stoweidlem17  46008  stoweidlem28  46019  fourierdlem12  46110  fourierdlem41  46139  fourierdlem42  46140  fourierdlem74  46171  fourierdlem77  46174  qndenserrnopnlem  46288  issalnnd  46336  hspmbllem2  46618  issmfle  46736  smflimlem2  46763  smflimmpt  46801  smfinflem  46808  smflimsuplem7  46817  smflimsupmpt  46820  smfliminfmpt  46823  lighneallem3  47601