Theorem 3ad2antl3 1206

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl3  1212  simpl3l  1247  simpl3r  1248  simpl31  1273  simpl32  1274  simpl33  1275  rspc3ev  3593  brcogw  5848  cocan1  7293  ov6g  7578  fpr1  8303  onelfvnef1  8431  dif1enlem  9157  dif1ennnALT  9250  cfsmolem  10275  coftr  10278  axcc3  10443  axdc4lem  10460  gruf  10823  dedekindle  11401  zdivmul  12696  cshf1  14884  cshimadifsn  14903  fprodle  16086  bpolycl  16141  lcmdvds  16701  lubss  18604  odeq  19680  ghmplusg  19976  lmhmvsca  21232  islindf4  22054  lindsenlbs  22067  mndifsplit  22861  gsummatr01lem3  22882  gsummatr01  22884  mp2pm2mplem4  23037  elcls  23301  cnpresti  23516  cmpsublem  23627  comppfsc  23761  ptpjcn  23840  elfm3  24179  rnelfmlem  24181  nmoix  24958  caublcls  25540  ig1pdvds  26408  coeid3  26469  amgm  27230  brbtwn2  29365  colinearalg  29370  axsegconlem1  29377  ax5seglem1  29388  ax5seglem2  29389  homco1  32285  hoadddi  32287  scottrankeqel  35634  br6  36339  upixp  38482  filbcmb  38493  3dim1  40343  llni  40384  lplni  40408  lvoli  40451  cdleme42mgN  41364  mzprename  43597  infmrgelbi  43722  relexpxpmin  44560  n0p  45882  rexabslelem  46249  pimxrneun  46319  limcleqr  46475  fnlimfvre  46505  stoweidlem17  46848  stoweidlem28  46859  fourierdlem12  46950  fourierdlem41  46979  fourierdlem42  46980  fourierdlem74  47011  fourierdlem77  47014  qndenserrnopnlem  47128  issalnnd  47176  hspmbllem2  47458  issmfle  47576  smflimlem2  47603  smflimmpt  47641  smfinflem  47648  smflimsuplem7  47657  smflimsupmpt  47660  smfliminfmpt  47663  lighneallem3  48513