Theorem 3ad2antl3 1204

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 1183	1 ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpl3  1210  simpl3l  1245  simpl3r  1246  simpl31  1271  simpl32  1272  simpl33  1273  rspc3ev  3607  brcogw  5855  cocan1  7290  ov6g  7575  fpr1  8300  dif1enlem  9144  dif1ennnALT  9237  cfsmolem  10254  coftr  10257  axcc3  10422  axdc4lem  10439  gruf  10796  dedekindle  11374  zdivmul  12668  cshf1  14847  cshimadifsn  14866  fprodle  16050  bpolycl  16106  lcmdvds  16666  lubss  18569  odeq  19620  ghmplusg  19916  lmhmvsca  21144  islindf4  21957  mndifsplit  22762  gsummatr01lem3  22783  gsummatr01  22785  mp2pm2mplem4  22935  elcls  23199  cnpresti  23414  cmpsublem  23525  comppfsc  23658  ptpjcn  23737  elfm3  24076  rnelfmlem  24078  nmoix  24855  caublcls  25437  ig1pdvds  26306  coeid3  26366  amgm  27121  brbtwn2  29196  colinearalg  29201  axsegconlem1  29208  ax5seglem1  29219  ax5seglem2  29220  homco1  32094  hoadddi  32096  br6  36182  lindsenlbs  38188  upixp  38302  filbcmb  38313  3dim1  40165  llni  40206  lplni  40230  lvoli  40273  cdleme42mgN  41186  mzprename  43406  infmrgelbi  43531  relexpxpmin  44369  n0p  45691  rexabslelem  46058  pimxrneun  46128  limcleqr  46284  fnlimfvre  46314  stoweidlem17  46657  stoweidlem28  46668  fourierdlem12  46759  fourierdlem41  46788  fourierdlem42  46789  fourierdlem74  46820  fourierdlem77  46823  qndenserrnopnlem  46937  issalnnd  46985  hspmbllem2  47267  issmfle  47385  smflimlem2  47412  smflimmpt  47450  smfinflem  47457  smflimsuplem7  47466  smflimsupmpt  47469  smfliminfmpt  47472  lighneallem3  48282