Theorem 3ad2antl3 1188

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 1167	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  1194  simpl3l  1229  simpl3r  1230  simpl31  1255  simpl32  1256  simpl33  1257  rspc3ev  3618  brcogw  5848  cocan1  7284  ov6g  7571  fpr1  8302  dif1enlem  9170  dif1ennnALT  9283  cfsmolem  10284  coftr  10287  axcc3  10452  axdc4lem  10469  gruf  10825  dedekindle  11399  zdivmul  12665  cshf1  14828  cshimadifsn  14848  fprodle  16012  bpolycl  16068  lcmdvds  16627  lubss  18523  odeq  19531  ghmplusg  19827  lmhmvsca  21003  islindf4  21798  mndifsplit  22574  gsummatr01lem3  22595  gsummatr01  22597  mp2pm2mplem4  22747  elcls  23011  cnpresti  23226  cmpsublem  23337  comppfsc  23470  ptpjcn  23549  elfm3  23888  rnelfmlem  23890  nmoix  24668  caublcls  25261  ig1pdvds  26137  coeid3  26197  amgm  26953  brbtwn2  28884  colinearalg  28889  axsegconlem1  28896  ax5seglem1  28907  ax5seglem2  28908  homco1  31782  hoadddi  31784  br6  35774  lindsenlbs  37639  upixp  37753  filbcmb  37764  3dim1  39486  llni  39527  lplni  39551  lvoli  39594  cdleme42mgN  40507  mzprename  42772  infmrgelbi  42901  relexpxpmin  43741  n0p  45069  rexabslelem  45445  pimxrneun  45515  limcleqr  45673  fnlimfvre  45703  stoweidlem17  46046  stoweidlem28  46057  fourierdlem12  46148  fourierdlem41  46177  fourierdlem42  46178  fourierdlem74  46209  fourierdlem77  46212  qndenserrnopnlem  46326  issalnnd  46374  hspmbllem2  46656  issmfle  46774  smflimlem2  46801  smflimmpt  46839  smfinflem  46846  smflimsuplem7  46855  smflimsupmpt  46858  smfliminfmpt  46861  lighneallem3  47621