Theorem 3ad2antl3 1189

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 715	. 2 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1168	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  1195  simpl3l  1230  simpl3r  1231  simpl31  1256  simpl32  1257  simpl33  1258  rspc3ev  3595  brcogw  5827  cocan1  7249  ov6g  7534  fpr1  8257  dif1enlem  9098  dif1ennnALT  9191  cfsmolem  10194  coftr  10197  axcc3  10362  axdc4lem  10379  gruf  10736  dedekindle  11311  zdivmul  12578  cshf1  14747  cshimadifsn  14766  fprodle  15933  bpolycl  15989  lcmdvds  16549  lubss  18450  odeq  19496  ghmplusg  19792  lmhmvsca  21014  islindf4  21810  mndifsplit  22597  gsummatr01lem3  22618  gsummatr01  22620  mp2pm2mplem4  22770  elcls  23034  cnpresti  23249  cmpsublem  23360  comppfsc  23493  ptpjcn  23572  elfm3  23911  rnelfmlem  23913  nmoix  24690  caublcls  25282  ig1pdvds  26158  coeid3  26218  amgm  26974  brbtwn2  28996  colinearalg  29001  axsegconlem1  29008  ax5seglem1  29019  ax5seglem2  29020  homco1  31895  hoadddi  31897  br6  35979  lindsenlbs  37895  upixp  38009  filbcmb  38020  3dim1  39872  llni  39913  lplni  39937  lvoli  39980  cdleme42mgN  40893  mzprename  43135  infmrgelbi  43264  relexpxpmin  44102  n0p  45434  rexabslelem  45805  pimxrneun  45875  limcleqr  46031  fnlimfvre  46061  stoweidlem17  46404  stoweidlem28  46415  fourierdlem12  46506  fourierdlem41  46535  fourierdlem42  46536  fourierdlem74  46567  fourierdlem77  46570  qndenserrnopnlem  46684  issalnnd  46732  hspmbllem2  47014  issmfle  47132  smflimlem2  47159  smflimmpt  47197  smfinflem  47204  smflimsuplem7  47213  smflimsupmpt  47216  smfliminfmpt  47219  lighneallem3  47996