Theorem 3ad2antl3 1185

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  simpl3  1191  simpl3l  1226  simpl3r  1227  simpl31  1252  simpl32  1253  simpl33  1254  rspc3ev  3627  brcogw  5867  cocan1  7291  ov6g  7573  fpr1  8290  dif1enlem  9158  dif1ennnALT  9279  cfsmolem  10267  coftr  10270  axcc3  10435  axdc4lem  10452  gruf  10808  dedekindle  11382  zdivmul  12638  cshf1  14764  cshimadifsn  14784  fprodle  15944  bpolycl  16000  lcmdvds  16549  lubss  18470  odeq  19459  ghmplusg  19755  lmhmvsca  20800  islindf4  21612  mndifsplit  22358  gsummatr01lem3  22379  gsummatr01  22381  mp2pm2mplem4  22531  elcls  22797  cnpresti  23012  cmpsublem  23123  comppfsc  23256  ptpjcn  23335  elfm3  23674  rnelfmlem  23676  nmoix  24466  caublcls  25057  ig1pdvds  25929  coeid3  25989  amgm  26731  brbtwn2  28430  colinearalg  28435  axsegconlem1  28442  ax5seglem1  28453  ax5seglem2  28454  homco1  31321  hoadddi  31323  br6  35031  lindsenlbs  36786  upixp  36900  filbcmb  36911  3dim1  38641  llni  38682  lplni  38706  lvoli  38749  cdleme42mgN  39662  mzprename  41789  infmrgelbi  41918  relexpxpmin  42770  n0p  44031  rexabslelem  44426  pimxrneun  44497  limcleqr  44658  fnlimfvre  44688  stoweidlem17  45031  stoweidlem28  45042  fourierdlem12  45133  fourierdlem41  45162  fourierdlem42  45163  fourierdlem74  45194  fourierdlem77  45197  qndenserrnopnlem  45311  issalnnd  45359  hspmbllem2  45641  issmfle  45759  smflimlem2  45786  smflimmpt  45824  smfinflem  45831  smflimsuplem7  45840  smflimsupmpt  45843  smfliminfmpt  45846  lighneallem3  46573