Theorem 3ad2antl3 1195

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  simpl3  1201  simpl3l  1236  simpl3r  1237  simpl31  1262  simpl32  1263  simpl33  1264  rspc3ev  3579  brcogw  5813  cocan1  7239  ov6g  7524  fpr1  8247  dif1enlem  9088  dif1ennnALT  9181  cfsmolem  10187  coftr  10190  axcc3  10355  axdc4lem  10372  gruf  10729  dedekindle  11305  zdivmul  12596  cshf1  14767  cshimadifsn  14786  fprodle  15956  bpolycl  16012  lcmdvds  16572  lubss  18474  odeq  19520  ghmplusg  19816  lmhmvsca  21039  islindf4  21817  mndifsplit  22623  gsummatr01lem3  22644  gsummatr01  22646  mp2pm2mplem4  22796  elcls  23060  cnpresti  23275  cmpsublem  23386  comppfsc  23519  ptpjcn  23598  elfm3  23937  rnelfmlem  23939  nmoix  24716  caublcls  25298  ig1pdvds  26167  coeid3  26227  amgm  26976  brbtwn2  28996  colinearalg  29001  axsegconlem1  29008  ax5seglem1  29019  ax5seglem2  29020  homco1  31894  hoadddi  31896  br6  36000  lindsenlbs  37997  upixp  38111  filbcmb  38122  3dim1  39974  llni  40015  lplni  40039  lvoli  40082  cdleme42mgN  40995  mzprename  43213  infmrgelbi  43338  relexpxpmin  44176  n0p  45508  rexabslelem  45875  pimxrneun  45945  limcleqr  46101  fnlimfvre  46131  stoweidlem17  46474  stoweidlem28  46485  fourierdlem12  46576  fourierdlem41  46605  fourierdlem42  46606  fourierdlem74  46637  fourierdlem77  46640  qndenserrnopnlem  46754  issalnnd  46802  hspmbllem2  47084  issmfle  47202  smflimlem2  47229  smflimmpt  47267  smfinflem  47274  smflimsuplem7  47283  smflimsupmpt  47286  smfliminfmpt  47289  lighneallem3  48099