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 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  1194  simpl3l  1229  simpl3r  1230  simpl31  1255  simpl32  1256  simpl33  1257  rspc3ev  3639  brcogw  5879  cocan1  7311  ov6g  7597  fpr1  8328  dif1enlem  9196  dif1ennnALT  9311  cfsmolem  10310  coftr  10313  axcc3  10478  axdc4lem  10495  gruf  10851  dedekindle  11425  zdivmul  12690  cshf1  14848  cshimadifsn  14868  fprodle  16032  bpolycl  16088  lcmdvds  16645  lubss  18558  odeq  19568  ghmplusg  19864  lmhmvsca  21044  islindf4  21858  mndifsplit  22642  gsummatr01lem3  22663  gsummatr01  22665  mp2pm2mplem4  22815  elcls  23081  cnpresti  23296  cmpsublem  23407  comppfsc  23540  ptpjcn  23619  elfm3  23958  rnelfmlem  23960  nmoix  24750  caublcls  25343  ig1pdvds  26219  coeid3  26279  amgm  27034  brbtwn2  28920  colinearalg  28925  axsegconlem1  28932  ax5seglem1  28943  ax5seglem2  28944  homco1  31820  hoadddi  31822  br6  35757  lindsenlbs  37622  upixp  37736  filbcmb  37747  3dim1  39469  llni  39510  lplni  39534  lvoli  39577  cdleme42mgN  40490  mzprename  42760  infmrgelbi  42889  relexpxpmin  43730  n0p  45050  rexabslelem  45429  pimxrneun  45499  limcleqr  45659  fnlimfvre  45689  stoweidlem17  46032  stoweidlem28  46043  fourierdlem12  46134  fourierdlem41  46163  fourierdlem42  46164  fourierdlem74  46195  fourierdlem77  46198  qndenserrnopnlem  46312  issalnnd  46360  hspmbllem2  46642  issmfle  46760  smflimlem2  46787  smflimmpt  46825  smfinflem  46832  smflimsuplem7  46841  smflimsupmpt  46844  smfliminfmpt  46847  lighneallem3  47594