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

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

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  simpl3  1195  simpl3l  1230  simpl3r  1231  simpl31  1256  simpl32  1257  simpl33  1258  rspc3ev  3541  brcogw  5722  cocan1  7079  ov6g  7350  fpr1  8021  dif1enOLD  8885  cfsmolem  9849  coftr  9852  axcc3  10017  axdc4lem  10034  gruf  10390  dedekindle  10961  zdivmul  12214  cshf1  14340  cshimadifsn  14359  fprodle  15521  bpolycl  15577  lcmdvds  16128  lubss  17973  gsumccatOLD  18221  odeq  18896  ghmplusg  19185  lmhmvsca  20036  islindf4  20754  mndifsplit  21487  gsummatr01lem3  21508  gsummatr01  21510  mp2pm2mplem4  21660  elcls  21924  cnpresti  22139  cmpsublem  22250  comppfsc  22383  ptpjcn  22462  elfm3  22801  rnelfmlem  22803  nmoix  23581  caublcls  24160  ig1pdvds  25028  coeid3  25088  amgm  25827  brbtwn2  26950  colinearalg  26955  axsegconlem1  26962  ax5seglem1  26973  ax5seglem2  26974  homco1  29836  hoadddi  29838  br6  33394  lindsenlbs  35458  upixp  35573  filbcmb  35584  3dim1  37167  llni  37208  lplni  37232  lvoli  37275  cdleme42mgN  38188  mzprename  40215  infmrgelbi  40344  relexpxpmin  40943  n0p  42205  rexabslelem  42572  limcleqr  42803  fnlimfvre  42833  stoweidlem17  43176  stoweidlem28  43187  fourierdlem12  43278  fourierdlem41  43307  fourierdlem42  43308  fourierdlem74  43339  fourierdlem77  43342  qndenserrnopnlem  43456  issalnnd  43502  hspmbllem2  43783  issmfle  43896  smflimlem2  43922  smflimmpt  43958  smfinflem  43965  smflimsuplem7  43974  smflimsupmpt  43977  smfliminfmpt  43980  lighneallem3  44675