Theorem 3ad2antl3 1189

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpl3  1195  simpl3l  1230  simpl3r  1231  simpl31  1256  simpl32  1257  simpl33  1258  rspc3ev  3594  brcogw  5818  cocan1  7239  ov6g  7524  fpr1  8247  dif1enlem  9088  dif1ennnALT  9181  cfsmolem  10184  coftr  10187  axcc3  10352  axdc4lem  10369  gruf  10726  dedekindle  11301  zdivmul  12568  cshf1  14737  cshimadifsn  14756  fprodle  15923  bpolycl  15979  lcmdvds  16539  lubss  18440  odeq  19483  ghmplusg  19779  lmhmvsca  21001  islindf4  21797  mndifsplit  22584  gsummatr01lem3  22605  gsummatr01  22607  mp2pm2mplem4  22757  elcls  23021  cnpresti  23236  cmpsublem  23347  comppfsc  23480  ptpjcn  23559  elfm3  23898  rnelfmlem  23900  nmoix  24677  caublcls  25269  ig1pdvds  26145  coeid3  26205  amgm  26961  brbtwn2  28982  colinearalg  28987  axsegconlem1  28994  ax5seglem1  29005  ax5seglem2  29006  homco1  31880  hoadddi  31882  br6  35953  lindsenlbs  37818  upixp  37932  filbcmb  37943  3dim1  39795  llni  39836  lplni  39860  lvoli  39903  cdleme42mgN  40816  mzprename  43058  infmrgelbi  43187  relexpxpmin  44025  n0p  45357  rexabslelem  45729  pimxrneun  45799  limcleqr  45955  fnlimfvre  45985  stoweidlem17  46328  stoweidlem28  46339  fourierdlem12  46430  fourierdlem41  46459  fourierdlem42  46460  fourierdlem74  46491  fourierdlem77  46494  qndenserrnopnlem  46608  issalnnd  46656  hspmbllem2  46938  issmfle  47056  smflimlem2  47083  smflimmpt  47121  smfinflem  47128  smflimsuplem7  47137  smflimsupmpt  47140  smfliminfmpt  47143  lighneallem3  47920