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  3637  brcogw  5739  cocan1  7047  ov6g  7312  dif1en  8751  cfsmolem  9692  coftr  9695  axcc3  9860  axdc4lem  9877  gruf  10233  dedekindle  10804  zdivmul  12055  cshf1  14172  cshimadifsn  14191  fprodle  15350  bpolycl  15406  lcmdvds  15952  lubss  17731  gsumccatOLD  18005  odeq  18678  ghmplusg  18966  lmhmvsca  19817  islindf4  20982  mndifsplit  21245  gsummatr01lem3  21266  gsummatr01  21268  mp2pm2mplem4  21417  elcls  21681  cnpresti  21896  cmpsublem  22007  comppfsc  22140  ptpjcn  22219  elfm3  22558  rnelfmlem  22560  nmoix  23338  caublcls  23912  ig1pdvds  24770  coeid3  24830  amgm  25568  brbtwn2  26691  colinearalg  26696  axsegconlem1  26703  ax5seglem1  26714  ax5seglem2  26715  homco1  29578  hoadddi  29580  br6  32993  fpr1  33139  lindsenlbs  34902  upixp  35019  filbcmb  35030  3dim1  36618  llni  36659  lplni  36683  lvoli  36726  cdleme42mgN  37639  mzprename  39395  infmrgelbi  39524  relexpxpmin  40111  n0p  41354  rexabslelem  41741  limcleqr  41974  fnlimfvre  42004  stoweidlem17  42351  stoweidlem28  42362  fourierdlem12  42453  fourierdlem41  42482  fourierdlem42  42483  fourierdlem74  42514  fourierdlem77  42517  qndenserrnopnlem  42631  issalnnd  42677  hspmbllem2  42958  issmfle  43071  smflimlem2  43097  smflimmpt  43133  smfinflem  43140  smflimsuplem7  43149  smflimsupmpt  43152  smfliminfmpt  43155  lighneallem3  43821