Theorem 3ad2antl3 1186

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 1165	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  1192  simpl3l  1227  simpl3r  1228  simpl31  1253  simpl32  1254  simpl33  1255  rspc3ev  3639  brcogw  5882  cocan1  7311  ov6g  7597  fpr1  8327  dif1enlem  9195  dif1ennnALT  9309  cfsmolem  10308  coftr  10311  axcc3  10476  axdc4lem  10493  gruf  10849  dedekindle  11423  zdivmul  12688  cshf1  14845  cshimadifsn  14865  fprodle  16029  bpolycl  16085  lcmdvds  16642  lubss  18571  odeq  19583  ghmplusg  19879  lmhmvsca  21062  islindf4  21876  mndifsplit  22658  gsummatr01lem3  22679  gsummatr01  22681  mp2pm2mplem4  22831  elcls  23097  cnpresti  23312  cmpsublem  23423  comppfsc  23556  ptpjcn  23635  elfm3  23974  rnelfmlem  23976  nmoix  24766  caublcls  25357  ig1pdvds  26234  coeid3  26294  amgm  27049  brbtwn2  28935  colinearalg  28940  axsegconlem1  28947  ax5seglem1  28958  ax5seglem2  28959  homco1  31830  hoadddi  31832  br6  35737  lindsenlbs  37602  upixp  37716  filbcmb  37727  3dim1  39450  llni  39491  lplni  39515  lvoli  39558  cdleme42mgN  40471  mzprename  42737  infmrgelbi  42866  relexpxpmin  43707  n0p  44983  rexabslelem  45368  pimxrneun  45439  limcleqr  45600  fnlimfvre  45630  stoweidlem17  45973  stoweidlem28  45984  fourierdlem12  46075  fourierdlem41  46104  fourierdlem42  46105  fourierdlem74  46136  fourierdlem77  46139  qndenserrnopnlem  46253  issalnnd  46301  hspmbllem2  46583  issmfle  46701  smflimlem2  46728  smflimmpt  46766  smfinflem  46773  smflimsuplem7  46782  smflimsupmpt  46785  smfliminfmpt  46788  lighneallem3  47532