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  3581  brcogw  5823  cocan1  7246  ov6g  7531  fpr1  8253  dif1enlem  9094  dif1ennnALT  9187  cfsmolem  10192  coftr  10195  axcc3  10360  axdc4lem  10377  gruf  10734  dedekindle  11310  zdivmul  12601  cshf1  14772  cshimadifsn  14791  fprodle  15961  bpolycl  16017  lcmdvds  16577  lubss  18479  odeq  19525  ghmplusg  19821  lmhmvsca  21040  islindf4  21818  mndifsplit  22601  gsummatr01lem3  22622  gsummatr01  22624  mp2pm2mplem4  22774  elcls  23038  cnpresti  23253  cmpsublem  23364  comppfsc  23497  ptpjcn  23576  elfm3  23915  rnelfmlem  23917  nmoix  24694  caublcls  25276  ig1pdvds  26145  coeid3  26205  amgm  26954  brbtwn2  28974  colinearalg  28979  axsegconlem1  28986  ax5seglem1  28997  ax5seglem2  28998  homco1  31872  hoadddi  31874  br6  35939  lindsenlbs  37936  upixp  38050  filbcmb  38061  3dim1  39913  llni  39954  lplni  39978  lvoli  40021  cdleme42mgN  40934  mzprename  43181  infmrgelbi  43306  relexpxpmin  44144  n0p  45476  rexabslelem  45846  pimxrneun  45916  limcleqr  46072  fnlimfvre  46102  stoweidlem17  46445  stoweidlem28  46456  fourierdlem12  46547  fourierdlem41  46576  fourierdlem42  46577  fourierdlem74  46608  fourierdlem77  46611  qndenserrnopnlem  46725  issalnnd  46773  hspmbllem2  47055  issmfle  47173  smflimlem2  47200  smflimmpt  47238  smfinflem  47245  smflimsuplem7  47254  smflimsupmpt  47257  smfliminfmpt  47260  lighneallem3  48070