Theorem 3ad2antl3 1189

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  simpl3  1195  simpl3l  1230  simpl3r  1231  simpl31  1256  simpl32  1257  simpl33  1258  rspc3ev  3582  brcogw  5819  cocan1  7241  ov6g  7526  fpr1  8248  dif1enlem  9089  dif1ennnALT  9182  cfsmolem  10187  coftr  10190  axcc3  10355  axdc4lem  10372  gruf  10729  dedekindle  11305  zdivmul  12596  cshf1  14767  cshimadifsn  14786  fprodle  15956  bpolycl  16012  lcmdvds  16572  lubss  18474  odeq  19520  ghmplusg  19816  lmhmvsca  21036  islindf4  21832  mndifsplit  22615  gsummatr01lem3  22636  gsummatr01  22638  mp2pm2mplem4  22788  elcls  23052  cnpresti  23267  cmpsublem  23378  comppfsc  23511  ptpjcn  23590  elfm3  23929  rnelfmlem  23931  nmoix  24708  caublcls  25290  ig1pdvds  26159  coeid3  26219  amgm  26972  brbtwn2  28992  colinearalg  28997  axsegconlem1  29004  ax5seglem1  29015  ax5seglem2  29016  homco1  31891  hoadddi  31893  br6  35959  lindsenlbs  37954  upixp  38068  filbcmb  38079  3dim1  39931  llni  39972  lplni  39996  lvoli  40039  cdleme42mgN  40952  mzprename  43199  infmrgelbi  43328  relexpxpmin  44166  n0p  45498  rexabslelem  45868  pimxrneun  45938  limcleqr  46094  fnlimfvre  46124  stoweidlem17  46467  stoweidlem28  46478  fourierdlem12  46569  fourierdlem41  46598  fourierdlem42  46599  fourierdlem74  46630  fourierdlem77  46633  qndenserrnopnlem  46747  issalnnd  46795  hspmbllem2  47077  issmfle  47195  smflimlem2  47222  smflimmpt  47260  smfinflem  47267  smflimsuplem7  47276  smflimsupmpt  47279  smfliminfmpt  47282  lighneallem3  48086