Theorem 3ad2antl3 1206

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is used by:  simpl3  1212  simpl3l  1247  simpl3r  1248  simpl31  1273  simpl32  1274  simpl33  1275  rspc3ev  3598  brcogw  5854  cocan1  7289  ov6g  7574  fpr1  8296  dif1enlem  9140  dif1ennnALT  9233  cfsmolem  10258  coftr  10261  axcc3  10426  axdc4lem  10443  gruf  10800  dedekindle  11378  zdivmul  12672  cshf1  14852  cshimadifsn  14871  fprodle  16055  bpolycl  16110  lcmdvds  16670  lubss  18573  odeq  19624  ghmplusg  19920  lmhmvsca  21175  islindf4  21997  mndifsplit  22802  gsummatr01lem3  22823  gsummatr01  22825  mp2pm2mplem4  22975  elcls  23239  cnpresti  23454  cmpsublem  23565  comppfsc  23698  ptpjcn  23777  elfm3  24116  rnelfmlem  24118  nmoix  24895  caublcls  25477  ig1pdvds  26346  coeid3  26406  amgm  27164  brbtwn2  29264  colinearalg  29269  axsegconlem1  29276  ax5seglem1  29287  ax5seglem2  29288  homco1  32162  hoadddi  32164  scottrankeqel  35526  br6  36257  lindsenlbs  38294  upixp  38408  filbcmb  38419  3dim1  40269  llni  40310  lplni  40334  lvoli  40377  cdleme42mgN  41290  mzprename  43508  infmrgelbi  43633  relexpxpmin  44471  n0p  45793  rexabslelem  46160  pimxrneun  46230  limcleqr  46386  fnlimfvre  46416  stoweidlem17  46759  stoweidlem28  46770  fourierdlem12  46861  fourierdlem41  46890  fourierdlem42  46891  fourierdlem74  46922  fourierdlem77  46925  qndenserrnopnlem  47039  issalnnd  47087  hspmbllem2  47369  issmfle  47487  smflimlem2  47514  smflimmpt  47552  smfinflem  47559  smflimsuplem7  47568  smflimsupmpt  47571  smfliminfmpt  47574  lighneallem3  48387