Theorem 3ad2antl3 1184

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 396  df-3an 1086

This theorem is referenced by:  simpl3  1190  simpl3l  1225  simpl3r  1226  simpl31  1251  simpl32  1252  simpl33  1253  rspc3ev  3623  brcogw  5862  cocan1  7285  ov6g  7568  fpr1  8289  dif1enlem  9158  dif1ennnALT  9279  cfsmolem  10267  coftr  10270  axcc3  10435  axdc4lem  10452  gruf  10808  dedekindle  11382  zdivmul  12638  cshf1  14766  cshimadifsn  14786  fprodle  15946  bpolycl  16002  lcmdvds  16552  lubss  18478  odeq  19470  ghmplusg  19766  lmhmvsca  20893  islindf4  21733  mndifsplit  22493  gsummatr01lem3  22514  gsummatr01  22516  mp2pm2mplem4  22666  elcls  22932  cnpresti  23147  cmpsublem  23258  comppfsc  23391  ptpjcn  23470  elfm3  23809  rnelfmlem  23811  nmoix  24601  caublcls  25192  ig1pdvds  26069  coeid3  26129  amgm  26878  brbtwn2  28671  colinearalg  28676  axsegconlem1  28683  ax5seglem1  28694  ax5seglem2  28695  homco1  31563  hoadddi  31565  br6  35260  lindsenlbs  36996  upixp  37110  filbcmb  37121  3dim1  38851  llni  38892  lplni  38916  lvoli  38959  cdleme42mgN  39872  mzprename  42065  infmrgelbi  42194  relexpxpmin  43044  n0p  44305  rexabslelem  44700  pimxrneun  44771  limcleqr  44932  fnlimfvre  44962  stoweidlem17  45305  stoweidlem28  45316  fourierdlem12  45407  fourierdlem41  45436  fourierdlem42  45437  fourierdlem74  45468  fourierdlem77  45471  qndenserrnopnlem  45585  issalnnd  45633  hspmbllem2  45915  issmfle  46033  smflimlem2  46060  smflimmpt  46098  smfinflem  46105  smflimsuplem7  46114  smflimsupmpt  46117  smfliminfmpt  46120  lighneallem3  46847