Theorem 3ad2antl3 1183

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpl3  1189  simpl3l  1224  simpl3r  1225  simpl31  1250  simpl32  1251  simpl33  1252  rspc3ev  3639  brcogw  5741  cocan1  7049  ov6g  7314  dif1en  8753  cfsmolem  9694  coftr  9697  axcc3  9862  axdc4lem  9879  gruf  10235  dedekindle  10806  zdivmul  12057  cshf1  14174  cshimadifsn  14193  fprodle  15352  bpolycl  15408  lcmdvds  15954  lubss  17733  gsumccatOLD  18007  odeq  18680  ghmplusg  18968  lmhmvsca  19819  islindf4  20984  mndifsplit  21247  gsummatr01lem3  21268  gsummatr01  21270  mp2pm2mplem4  21419  elcls  21683  cnpresti  21898  cmpsublem  22009  comppfsc  22142  ptpjcn  22221  elfm3  22560  rnelfmlem  22562  nmoix  23340  caublcls  23914  ig1pdvds  24772  coeid3  24832  amgm  25570  brbtwn2  26693  colinearalg  26698  axsegconlem1  26705  ax5seglem1  26716  ax5seglem2  26717  homco1  29580  hoadddi  29582  br6  32995  fpr1  33141  lindsenlbs  34889  upixp  35006  filbcmb  35017  3dim1  36605  llni  36646  lplni  36670  lvoli  36713  cdleme42mgN  37626  mzprename  39353  infmrgelbi  39482  relexpxpmin  40069  n0p  41312  rexabslelem  41699  limcleqr  41932  fnlimfvre  41962  stoweidlem17  42309  stoweidlem28  42320  fourierdlem12  42411  fourierdlem41  42440  fourierdlem42  42441  fourierdlem74  42472  fourierdlem77  42475  qndenserrnopnlem  42589  issalnnd  42635  hspmbllem2  42916  issmfle  43029  smflimlem2  43055  smflimmpt  43091  smfinflem  43098  smflimsuplem7  43107  smflimsupmpt  43110  smfliminfmpt  43113  lighneallem3  43779