Theorem 3ad2antl3 1202

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  simpl3  1208  simpl3l  1243  simpl3r  1244  simpl31  1269  simpl32  1270  simpl33  1271  rspc3ev  3600  brcogw  5842  cocan1  7277  ov6g  7562  fpr1  8286  dif1enlem  9130  dif1ennnALT  9223  cfsmolem  10229  coftr  10232  axcc3  10397  axdc4lem  10414  gruf  10771  dedekindle  11349  zdivmul  12647  cshf1  14825  cshimadifsn  14844  fprodle  16028  bpolycl  16084  lcmdvds  16644  lubss  18547  odeq  19592  ghmplusg  19888  lmhmvsca  21114  islindf4  21892  mndifsplit  22698  gsummatr01lem3  22719  gsummatr01  22721  mp2pm2mplem4  22871  elcls  23135  cnpresti  23350  cmpsublem  23461  comppfsc  23594  ptpjcn  23673  elfm3  24012  rnelfmlem  24014  nmoix  24791  caublcls  25373  ig1pdvds  26242  coeid3  26302  amgm  27057  brbtwn2  29108  colinearalg  29113  axsegconlem1  29120  ax5seglem1  29131  ax5seglem2  29132  homco1  32006  hoadddi  32008  br6  36112  lindsenlbs  38119  upixp  38233  filbcmb  38244  3dim1  40096  llni  40137  lplni  40161  lvoli  40204  cdleme42mgN  41117  mzprename  43335  infmrgelbi  43460  relexpxpmin  44298  n0p  45630  rexabslelem  45997  pimxrneun  46067  limcleqr  46223  fnlimfvre  46253  stoweidlem17  46596  stoweidlem28  46607  fourierdlem12  46698  fourierdlem41  46727  fourierdlem42  46728  fourierdlem74  46759  fourierdlem77  46762  qndenserrnopnlem  46876  issalnnd  46924  hspmbllem2  47206  issmfle  47324  smflimlem2  47351  smflimmpt  47389  smfinflem  47396  smflimsuplem7  47405  smflimsupmpt  47408  smfliminfmpt  47411  lighneallem3  48221