Theorem 3ad2antl3 1225

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  rspc3ev  3326  brcogw  5290  cocan1  6546  ov6g  6798  dif1en  8193  cfsmolem  9092  coftr  9095  axcc3  9260  axdc4lem  9277  gruf  9633  dedekindle  10201  zdivmul  11449  cshimadifsn  13575  fprodle  14727  bpolycl  14783  lcmdvds  15321  coprmdvdsOLD  15367  lubss  17121  gsumccat  17378  odeq  17969  ghmplusg  18249  lmhmvsca  19045  islindf4  20177  mndifsplit  20442  gsummatr01lem3  20463  gsummatr01  20465  mp2pm2mplem4  20614  elcls  20877  cnpresti  21092  cmpsublem  21202  comppfsc  21335  ptpjcn  21414  elfm3  21754  rnelfmlem  21756  nmoix  22533  caublcls  23107  ig1pdvds  23936  coeid3  23996  amgm  24717  brbtwn2  25785  colinearalg  25790  axsegconlem1  25797  ax5seglem1  25808  ax5seglem2  25809  edginwlkOLD  26531  homco1  28660  hoadddi  28662  br6  31647  lindsenlbs  33404  upixp  33524  filbcmb  33535  3dim1  34753  llni  34794  lplni  34818  lvoli  34861  cdleme42mgN  35776  mzprename  37312  infmrgelbi  37442  relexpxpmin  38009  n0p  39209  rexabslelem  39645  limcleqr  39876  fnlimfvre  39906  stoweidlem17  40234  stoweidlem28  40245  fourierdlem12  40336  fourierdlem41  40365  fourierdlem42  40366  fourierdlem74  40397  fourierdlem77  40400  qndenserrnopnlem  40517  issalnnd  40563  hspmbllem2  40841  issmfle  40954  smflimlem2  40980  smflimmpt  41016  smfinflem  41023  smflimsuplem7  41032  smflimsupmpt  41035  smfliminfmpt  41038  lighneallem3  41524