Theorem 3ad2antl3 1187

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpl3  1193  simpl3l  1228  simpl3r  1229  simpl31  1254  simpl32  1255  simpl33  1256  rspc3ev  3595  brcogw  5829  cocan1  7242  ov6g  7523  fpr1  8239  dif1enlem  9107  dif1ennnALT  9228  cfsmolem  10215  coftr  10218  axcc3  10383  axdc4lem  10400  gruf  10756  dedekindle  11328  zdivmul  12584  cshf1  14710  cshimadifsn  14730  fprodle  15890  bpolycl  15946  lcmdvds  16495  lubss  18416  odeq  19346  ghmplusg  19638  lmhmvsca  20563  islindf4  21281  mndifsplit  22022  gsummatr01lem3  22043  gsummatr01  22045  mp2pm2mplem4  22195  elcls  22461  cnpresti  22676  cmpsublem  22787  comppfsc  22920  ptpjcn  22999  elfm3  23338  rnelfmlem  23340  nmoix  24130  caublcls  24710  ig1pdvds  25578  coeid3  25638  amgm  26377  brbtwn2  27917  colinearalg  27922  axsegconlem1  27929  ax5seglem1  27940  ax5seglem2  27941  homco1  30806  hoadddi  30808  br6  34416  lindsenlbs  36146  upixp  36261  filbcmb  36272  3dim1  38003  llni  38044  lplni  38068  lvoli  38111  cdleme42mgN  39024  mzprename  41130  infmrgelbi  41259  relexpxpmin  42111  n0p  43373  rexabslelem  43773  pimxrneun  43844  limcleqr  44005  fnlimfvre  44035  stoweidlem17  44378  stoweidlem28  44389  fourierdlem12  44480  fourierdlem41  44509  fourierdlem42  44510  fourierdlem74  44541  fourierdlem77  44544  qndenserrnopnlem  44658  issalnnd  44706  hspmbllem2  44988  issmfle  45106  smflimlem2  45133  smflimmpt  45171  smfinflem  45178  smflimsuplem7  45187  smflimsupmpt  45190  smfliminfmpt  45193  lighneallem3  45919