Theorem 3ad2antl3 1188

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

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

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 1088

This theorem is referenced by:  simpl3  1194  simpl3l  1229  simpl3r  1230  simpl31  1255  simpl32  1256  simpl33  1257  rspc3ev  3591  brcogw  5815  cocan1  7235  ov6g  7520  fpr1  8243  dif1enlem  9082  dif1ennnALT  9175  cfsmolem  10178  coftr  10181  axcc3  10346  axdc4lem  10363  gruf  10720  dedekindle  11295  zdivmul  12562  cshf1  14731  cshimadifsn  14750  fprodle  15917  bpolycl  15973  lcmdvds  16533  lubss  18434  odeq  19477  ghmplusg  19773  lmhmvsca  20995  islindf4  21791  mndifsplit  22578  gsummatr01lem3  22599  gsummatr01  22601  mp2pm2mplem4  22751  elcls  23015  cnpresti  23230  cmpsublem  23341  comppfsc  23474  ptpjcn  23553  elfm3  23892  rnelfmlem  23894  nmoix  24671  caublcls  25263  ig1pdvds  26139  coeid3  26199  amgm  26955  brbtwn2  28927  colinearalg  28932  axsegconlem1  28939  ax5seglem1  28950  ax5seglem2  28951  homco1  31825  hoadddi  31827  br6  35900  lindsenlbs  37755  upixp  37869  filbcmb  37880  3dim1  39666  llni  39707  lplni  39731  lvoli  39774  cdleme42mgN  40687  mzprename  42933  infmrgelbi  43062  relexpxpmin  43900  n0p  45232  rexabslelem  45604  pimxrneun  45674  limcleqr  45830  fnlimfvre  45860  stoweidlem17  46203  stoweidlem28  46214  fourierdlem12  46305  fourierdlem41  46334  fourierdlem42  46335  fourierdlem74  46366  fourierdlem77  46369  qndenserrnopnlem  46483  issalnnd  46531  hspmbllem2  46813  issmfle  46931  smflimlem2  46958  smflimmpt  46996  smfinflem  47003  smflimsuplem7  47012  smflimsupmpt  47015  smfliminfmpt  47018  lighneallem3  47795