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  3596  brcogw  5852  cocan1  7296  ov6g  7581  fpr1  8306  dif1enlem  9158  dif1ennnALT  9251  cfsmolem  10276  coftr  10279  axcc3  10444  axdc4lem  10461  gruf  10824  dedekindle  11402  zdivmul  12697  cshf1  14885  cshimadifsn  14904  fprodle  16089  bpolycl  16144  lcmdvds  16704  lubss  18607  odeq  19683  ghmplusg  19979  lmhmvsca  21235  islindf4  22057  lindsenlbs  22070  mndifsplit  22864  gsummatr01lem3  22885  gsummatr01  22887  mp2pm2mplem4  23040  elcls  23304  cnpresti  23519  cmpsublem  23630  comppfsc  23764  ptpjcn  23843  elfm3  24182  rnelfmlem  24184  nmoix  24961  caublcls  25543  ig1pdvds  26412  coeid3  26473  amgm  27235  brbtwn2  29370  colinearalg  29375  axsegconlem1  29382  ax5seglem1  29393  ax5seglem2  29394  homco1  32290  hoadddi  32292  scottrankeqel  35639  br6  36344  upixp  38487  filbcmb  38498  3dim1  40348  llni  40389  lplni  40413  lvoli  40456  cdleme42mgN  41369  mzprename  43602  infmrgelbi  43727  relexpxpmin  44565  n0p  45887  rexabslelem  46254  pimxrneun  46324  limcleqr  46480  fnlimfvre  46510  stoweidlem17  46853  stoweidlem28  46864  fourierdlem12  46955  fourierdlem41  46984  fourierdlem42  46985  fourierdlem74  47016  fourierdlem77  47019  qndenserrnopnlem  47133  issalnnd  47181  hspmbllem2  47463  issmfle  47581  smflimlem2  47608  smflimmpt  47646  smfinflem  47653  smflimsuplem7  47662  smflimsupmpt  47665  smfliminfmpt  47668  lighneallem3  48518