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  3593  brcogw  5817  cocan1  7237  ov6g  7522  fpr1  8245  dif1enlem  9084  dif1ennnALT  9177  cfsmolem  10180  coftr  10183  axcc3  10348  axdc4lem  10365  gruf  10722  dedekindle  11297  zdivmul  12564  cshf1  14733  cshimadifsn  14752  fprodle  15919  bpolycl  15975  lcmdvds  16535  lubss  18436  odeq  19479  ghmplusg  19775  lmhmvsca  20997  islindf4  21793  mndifsplit  22580  gsummatr01lem3  22601  gsummatr01  22603  mp2pm2mplem4  22753  elcls  23017  cnpresti  23232  cmpsublem  23343  comppfsc  23476  ptpjcn  23555  elfm3  23894  rnelfmlem  23896  nmoix  24673  caublcls  25265  ig1pdvds  26141  coeid3  26201  amgm  26957  brbtwn2  28978  colinearalg  28983  axsegconlem1  28990  ax5seglem1  29001  ax5seglem2  29002  homco1  31876  hoadddi  31878  br6  35951  lindsenlbs  37812  upixp  37926  filbcmb  37937  3dim1  39723  llni  39764  lplni  39788  lvoli  39831  cdleme42mgN  40744  mzprename  42987  infmrgelbi  43116  relexpxpmin  43954  n0p  45286  rexabslelem  45658  pimxrneun  45728  limcleqr  45884  fnlimfvre  45914  stoweidlem17  46257  stoweidlem28  46268  fourierdlem12  46359  fourierdlem41  46388  fourierdlem42  46389  fourierdlem74  46420  fourierdlem77  46423  qndenserrnopnlem  46537  issalnnd  46585  hspmbllem2  46867  issmfle  46985  smflimlem2  47012  smflimmpt  47050  smfinflem  47057  smflimsuplem7  47066  smflimsupmpt  47069  smfliminfmpt  47072  lighneallem3  47849