Theorem 3ad2antl3 1186

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 1165	1 ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpl3  1192  simpl3l  1227  simpl3r  1228  simpl31  1253  simpl32  1254  simpl33  1255  rspc3ev  3583  brcogw  5810  cocan1  7219  ov6g  7498  fpr1  8189  dif1enlem  9021  dif1ennnALT  9142  cfsmolem  10127  coftr  10130  axcc3  10295  axdc4lem  10312  gruf  10668  dedekindle  11240  zdivmul  12493  cshf1  14621  cshimadifsn  14641  fprodle  15805  bpolycl  15861  lcmdvds  16410  lubss  18328  odeq  19254  ghmplusg  19542  lmhmvsca  20413  islindf4  21151  mndifsplit  21891  gsummatr01lem3  21912  gsummatr01  21914  mp2pm2mplem4  22064  elcls  22330  cnpresti  22545  cmpsublem  22656  comppfsc  22789  ptpjcn  22868  elfm3  23207  rnelfmlem  23209  nmoix  23999  caublcls  24579  ig1pdvds  25447  coeid3  25507  amgm  26246  brbtwn2  27562  colinearalg  27567  axsegconlem1  27574  ax5seglem1  27585  ax5seglem2  27586  homco1  30451  hoadddi  30453  br6  34013  lindsenlbs  35877  upixp  35992  filbcmb  36003  3dim1  37735  llni  37776  lplni  37800  lvoli  37843  cdleme42mgN  38756  mzprename  40833  infmrgelbi  40962  relexpxpmin  41646  n0p  42911  rexabslelem  43293  pimxrneun  43364  limcleqr  43521  fnlimfvre  43551  stoweidlem17  43894  stoweidlem28  43905  fourierdlem12  43996  fourierdlem41  44025  fourierdlem42  44026  fourierdlem74  44057  fourierdlem77  44060  qndenserrnopnlem  44174  issalnnd  44220  hspmbllem2  44502  issmfle  44620  smflimlem2  44647  smflimmpt  44685  smfinflem  44692  smflimsuplem7  44701  smflimsupmpt  44704  smfliminfmpt  44707  lighneallem3  45410