Theorem 3ad2antl3 1185

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

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

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 396  df-3an 1087

This theorem is referenced by:  simpl3  1191  simpl3l  1226  simpl3r  1227  simpl31  1252  simpl32  1253  simpl33  1254  rspc3ev  3566  brcogw  5766  cocan1  7143  ov6g  7414  fpr1  8090  dif1enALT  8980  cfsmolem  9957  coftr  9960  axcc3  10125  axdc4lem  10142  gruf  10498  dedekindle  11069  zdivmul  12322  cshf1  14451  cshimadifsn  14470  fprodle  15634  bpolycl  15690  lcmdvds  16241  lubss  18146  gsumccatOLD  18394  odeq  19073  ghmplusg  19362  lmhmvsca  20222  islindf4  20955  mndifsplit  21693  gsummatr01lem3  21714  gsummatr01  21716  mp2pm2mplem4  21866  elcls  22132  cnpresti  22347  cmpsublem  22458  comppfsc  22591  ptpjcn  22670  elfm3  23009  rnelfmlem  23011  nmoix  23799  caublcls  24378  ig1pdvds  25246  coeid3  25306  amgm  26045  brbtwn2  27176  colinearalg  27181  axsegconlem1  27188  ax5seglem1  27199  ax5seglem2  27200  homco1  30064  hoadddi  30066  br6  33630  lindsenlbs  35699  upixp  35814  filbcmb  35825  3dim1  37408  llni  37449  lplni  37473  lvoli  37516  cdleme42mgN  38429  mzprename  40487  infmrgelbi  40616  relexpxpmin  41214  n0p  42480  rexabslelem  42848  limcleqr  43075  fnlimfvre  43105  stoweidlem17  43448  stoweidlem28  43459  fourierdlem12  43550  fourierdlem41  43579  fourierdlem42  43580  fourierdlem74  43611  fourierdlem77  43614  qndenserrnopnlem  43728  issalnnd  43774  hspmbllem2  44055  issmfle  44168  smflimlem2  44194  smflimmpt  44230  smfinflem  44237  smflimsuplem7  44246  smflimsupmpt  44249  smfliminfmpt  44252  lighneallem3  44947