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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ 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 402  df-3an 1105

This theorem is used by:  simpl3  1212  simpl3l  1247  simpl3r  1248  simpl31  1273  simpl32  1274  simpl33  1275  rspc3ev  3593  brcogw  5846  cocan1  7299  ov6g  7584  fpr1  8321  onelfvnef1  8449  dif1enlem  9175  dif1ennnALT  9268  cfsmolem  10348  coftr  10351  axcc3  10516  axdc4lem  10533  gruf  10896  dedekindle  11474  zdivmul  12771  cshf1  14961  cshimadifsn  14980  fprodle  16163  bpolycl  16218  lcmdvds  16783  lubss  18687  odeq  19764  ghmplusg  20060  lmhmvsca  21320  islindf4  22144  lindsenlbs  22157  mndifsplit  22951  gsummatr01lem3  22972  gsummatr01  22974  mp2pm2mplem4  23127  elcls  23391  cnpresti  23606  cmpsublem  23717  comppfsc  23851  ptpjcn  23930  elfm3  24269  rnelfmlem  24271  nmoix  25048  caublcls  25630  ig1pdvds  26498  coeid3  26559  amgm  27318  brbtwn2  29483  colinearalg  29488  axsegconlem1  29495  ax5seglem1  29506  ax5seglem2  29507  homco1  32403  hoadddi  32405  scottrankeqel  35748  br6  36522  upixp  38663  filbcmb  38674  3dim1  40524  llni  40565  lplni  40589  lvoli  40632  cdleme42mgN  41545  mzprename  43759  infmrgelbi  43884  relexpxpmin  44716  n0p  46061  rexabslelem  46427  pimxrneun  46497  limcleqr  46653  fnlimfvre  46683  stoweidlem17  47026  stoweidlem28  47037  fourierdlem12  47128  fourierdlem41  47157  fourierdlem42  47158  fourierdlem74  47189  fourierdlem77  47192  qndenserrnopnlem  47306  issalnnd  47354  hspmbllem2  47636  issmfle  47754  smflimlem2  47781  smflimmpt  47819  smfinflem  47826  smflimsuplem7  47835  smflimsupmpt  47838  smfliminfmpt  47841  lighneallem3  48691