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  3608  brcogw  5835  cocan1  7269  ov6g  7556  fpr1  8285  dif1enlem  9126  dif1ennnALT  9229  cfsmolem  10230  coftr  10233  axcc3  10398  axdc4lem  10415  gruf  10771  dedekindle  11345  zdivmul  12613  cshf1  14782  cshimadifsn  14802  fprodle  15969  bpolycl  16025  lcmdvds  16585  lubss  18479  odeq  19487  ghmplusg  19783  lmhmvsca  20959  islindf4  21754  mndifsplit  22530  gsummatr01lem3  22551  gsummatr01  22553  mp2pm2mplem4  22703  elcls  22967  cnpresti  23182  cmpsublem  23293  comppfsc  23426  ptpjcn  23505  elfm3  23844  rnelfmlem  23846  nmoix  24624  caublcls  25216  ig1pdvds  26092  coeid3  26152  amgm  26908  brbtwn2  28839  colinearalg  28844  axsegconlem1  28851  ax5seglem1  28862  ax5seglem2  28863  homco1  31737  hoadddi  31739  br6  35751  lindsenlbs  37616  upixp  37730  filbcmb  37741  3dim1  39468  llni  39509  lplni  39533  lvoli  39576  cdleme42mgN  40489  mzprename  42744  infmrgelbi  42873  relexpxpmin  43713  n0p  45046  rexabslelem  45421  pimxrneun  45491  limcleqr  45649  fnlimfvre  45679  stoweidlem17  46022  stoweidlem28  46033  fourierdlem12  46124  fourierdlem41  46153  fourierdlem42  46154  fourierdlem74  46185  fourierdlem77  46188  qndenserrnopnlem  46302  issalnnd  46350  hspmbllem2  46632  issmfle  46750  smflimlem2  46777  smflimmpt  46815  smfinflem  46822  smflimsuplem7  46831  smflimsupmpt  46834  smfliminfmpt  46837  lighneallem3  47612