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  3589  brcogw  5807  cocan1  7225  ov6g  7510  fpr1  8233  dif1enlem  9069  dif1ennnALT  9161  cfsmolem  10161  coftr  10164  axcc3  10329  axdc4lem  10346  gruf  10702  dedekindle  11277  zdivmul  12545  cshf1  14717  cshimadifsn  14736  fprodle  15903  bpolycl  15959  lcmdvds  16519  lubss  18419  odeq  19462  ghmplusg  19758  lmhmvsca  20979  islindf4  21775  mndifsplit  22551  gsummatr01lem3  22572  gsummatr01  22574  mp2pm2mplem4  22724  elcls  22988  cnpresti  23203  cmpsublem  23314  comppfsc  23447  ptpjcn  23526  elfm3  23865  rnelfmlem  23867  nmoix  24644  caublcls  25236  ig1pdvds  26112  coeid3  26172  amgm  26928  brbtwn2  28883  colinearalg  28888  axsegconlem1  28895  ax5seglem1  28906  ax5seglem2  28907  homco1  31781  hoadddi  31783  br6  35801  lindsenlbs  37654  upixp  37768  filbcmb  37779  3dim1  39565  llni  39606  lplni  39630  lvoli  39673  cdleme42mgN  40586  mzprename  42841  infmrgelbi  42970  relexpxpmin  43809  n0p  45141  rexabslelem  45515  pimxrneun  45585  limcleqr  45741  fnlimfvre  45771  stoweidlem17  46114  stoweidlem28  46125  fourierdlem12  46216  fourierdlem41  46245  fourierdlem42  46246  fourierdlem74  46277  fourierdlem77  46280  qndenserrnopnlem  46394  issalnnd  46442  hspmbllem2  46724  issmfle  46842  smflimlem2  46869  smflimmpt  46907  smfinflem  46914  smflimsuplem7  46923  smflimsupmpt  46926  smfliminfmpt  46929  lighneallem3  47706