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  3600  brcogw  5856  cocan1  7298  ov6g  7583  fpr1  8306  dif1enlem  9151  dif1ennnALT  9244  cfsmolem  10269  coftr  10272  axcc3  10437  axdc4lem  10454  gruf  10815  dedekindle  11393  zdivmul  12688  cshf1  14875  cshimadifsn  14894  fprodle  16077  bpolycl  16132  lcmdvds  16692  lubss  18595  odeq  19668  ghmplusg  19964  lmhmvsca  21220  islindf4  22042  mndifsplit  22847  gsummatr01lem3  22868  gsummatr01  22870  mp2pm2mplem4  23020  elcls  23284  cnpresti  23499  cmpsublem  23610  comppfsc  23744  ptpjcn  23823  elfm3  24162  rnelfmlem  24164  nmoix  24941  caublcls  25523  ig1pdvds  26392  coeid3  26452  amgm  27210  brbtwn2  29314  colinearalg  29319  axsegconlem1  29326  ax5seglem1  29337  ax5seglem2  29338  homco1  32228  hoadddi  32230  scottrankeqel  35579  br6  36290  lindsenlbs  38327  upixp  38442  filbcmb  38453  3dim1  40303  llni  40344  lplni  40368  lvoli  40411  cdleme42mgN  41324  mzprename  43557  infmrgelbi  43682  relexpxpmin  44520  n0p  45842  rexabslelem  46209  pimxrneun  46279  limcleqr  46435  fnlimfvre  46465  stoweidlem17  46808  stoweidlem28  46819  fourierdlem12  46910  fourierdlem41  46939  fourierdlem42  46940  fourierdlem74  46971  fourierdlem77  46974  qndenserrnopnlem  47088  issalnnd  47136  hspmbllem2  47418  issmfle  47536  smflimlem2  47563  smflimmpt  47601  smfinflem  47608  smflimsuplem7  47617  smflimsupmpt  47620  smfliminfmpt  47623  lighneallem3  48436