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  3605  brcogw  5832  cocan1  7266  ov6g  7553  fpr1  8282  dif1enlem  9120  dif1ennnALT  9222  cfsmolem  10223  coftr  10226  axcc3  10391  axdc4lem  10408  gruf  10764  dedekindle  11338  zdivmul  12606  cshf1  14775  cshimadifsn  14795  fprodle  15962  bpolycl  16018  lcmdvds  16578  lubss  18472  odeq  19480  ghmplusg  19776  lmhmvsca  20952  islindf4  21747  mndifsplit  22523  gsummatr01lem3  22544  gsummatr01  22546  mp2pm2mplem4  22696  elcls  22960  cnpresti  23175  cmpsublem  23286  comppfsc  23419  ptpjcn  23498  elfm3  23837  rnelfmlem  23839  nmoix  24617  caublcls  25209  ig1pdvds  26085  coeid3  26145  amgm  26901  brbtwn2  28832  colinearalg  28837  axsegconlem1  28844  ax5seglem1  28855  ax5seglem2  28856  homco1  31730  hoadddi  31732  br6  35744  lindsenlbs  37609  upixp  37723  filbcmb  37734  3dim1  39461  llni  39502  lplni  39526  lvoli  39569  cdleme42mgN  40482  mzprename  42737  infmrgelbi  42866  relexpxpmin  43706  n0p  45039  rexabslelem  45414  pimxrneun  45484  limcleqr  45642  fnlimfvre  45672  stoweidlem17  46015  stoweidlem28  46026  fourierdlem12  46117  fourierdlem41  46146  fourierdlem42  46147  fourierdlem74  46178  fourierdlem77  46181  qndenserrnopnlem  46295  issalnnd  46343  hspmbllem2  46625  issmfle  46743  smflimlem2  46770  smflimmpt  46808  smfinflem  46815  smflimsuplem7  46824  smflimsupmpt  46827  smfliminfmpt  46830  lighneallem3  47608