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  3602  brcogw  5822  cocan1  7248  ov6g  7533  fpr1  8259  dif1enlem  9097  dif1ennnALT  9198  cfsmolem  10199  coftr  10202  axcc3  10367  axdc4lem  10384  gruf  10740  dedekindle  11314  zdivmul  12582  cshf1  14751  cshimadifsn  14771  fprodle  15938  bpolycl  15994  lcmdvds  16554  lubss  18454  odeq  19464  ghmplusg  19760  lmhmvsca  20984  islindf4  21780  mndifsplit  22556  gsummatr01lem3  22577  gsummatr01  22579  mp2pm2mplem4  22729  elcls  22993  cnpresti  23208  cmpsublem  23319  comppfsc  23452  ptpjcn  23531  elfm3  23870  rnelfmlem  23872  nmoix  24650  caublcls  25242  ig1pdvds  26118  coeid3  26178  amgm  26934  brbtwn2  28885  colinearalg  28890  axsegconlem1  28897  ax5seglem1  28908  ax5seglem2  28909  homco1  31780  hoadddi  31782  br6  35737  lindsenlbs  37602  upixp  37716  filbcmb  37727  3dim1  39454  llni  39495  lplni  39519  lvoli  39562  cdleme42mgN  40475  mzprename  42730  infmrgelbi  42859  relexpxpmin  43699  n0p  45032  rexabslelem  45407  pimxrneun  45477  limcleqr  45635  fnlimfvre  45665  stoweidlem17  46008  stoweidlem28  46019  fourierdlem12  46110  fourierdlem41  46139  fourierdlem42  46140  fourierdlem74  46171  fourierdlem77  46174  qndenserrnopnlem  46288  issalnnd  46336  hspmbllem2  46618  issmfle  46736  smflimlem2  46763  smflimmpt  46801  smfinflem  46808  smflimsuplem7  46817  smflimsupmpt  46820  smfliminfmpt  46823  lighneallem3  47601