Theorem 3ad2antl1 1204

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antl1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 727	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1186	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simpl1  1210  simpl1l  1243  simpl1r  1244  simpl11  1267  simpl12  1268  simpl13  1269  smocdmdom  8351  omeulem1  8563  f1oen4g  8957  f1dom4g  8958  dif1ennnALT  9233  ordiso2  9473  infpssrlem4  10285  fin1a2lem9  10387  gchpwdom  10650  tskwun  10764  gruxp  10787  infregelb  12194  fzo1fzo0n0  13740  fsuppmapnn0fiub  14023  pfxsuffeqwrdeq  14731  fprodle  16046  muldvds2  16334  dvds2add  16343  dvds2sub  16344  dvdstr  16347  lcmfledvds  16685  mndvcl  18850  mhmvlin  18854  mulgnnsubcl  19147  mulgpropd  19177  gexdvdsi  19648  ringidss  20356  reslmhm2  21174  obs2ss  21879  lsslindf  21980  issubassa  22017  madurid  22801  restntr  23339  cnpnei  23421  upxp  23780  qtopss  23872  opnfbas  23999  fbasrn  24041  trfg  24048  ufilmax  24064  ustuqtop1  24398  prdsxmetlem  24525  nmoix  24886  nmoi2  24887  iimulcl  25096  mbfimaopn2  25816  lgsval4lem  27472  nodenselem8  27855  f1otrg  29220  brbtwn2  29255  colinearalg  29260  axsegconlem1  29267  0vtxrusgr  29927  clwwlkccatlem  30340  clwwlkccat  30341  clwwisshclwws  30366  clwwlkfo  30401  numclwwlk1lem2fo  30709  lnosub  31111  pjspansn  31929  eulerpartlemb  34758  cnpconn  35722  mclspps  36076  curf  38269  mblfinlem2  38329  mblfinlem3  38330  mettrifi  38428  ghomdiv  38563  grpokerinj  38564  rngohomco  38645  crngohomfo  38677  keridl  38703  cvrcon3b  40071  mzpsubst  43499  lzunuz  43519  diophrex  43526  rmxycomplete  43664  jm2.26  43749  lnmepi  43832  lmhmlnmsplit  43834  nadd2rabex  44133  nadd1rabtr  44135  nadd1rabex  44137  ntrclsiso  44813  ntrclskb  44815  ntrclsk3  44816  uzwo4  45793  wessf1ornlem  45923  choicefi  45937  supxrgere  46069  supxrgelem  46073  supxrge  46074  suplesup  46075  infxr  46102  infleinflem2  46106  rexabslelem  46152  fmul01lt1  46322  limcleqr  46378  limclner  46385  dvnprodlem1  46680  volioc  46706  stoweidlem60  46794  wallispilem3  46801  fourierdlem12  46853  fourierdlem41  46882  fourierdlem42  46883  fourierdlem48  46888  fourierdlem49  46889  fourierdlem54  46894  fourierdlem68  46908  fourierdlem73  46913  fourierdlem74  46914  fourierdlem75  46915  fourierdlem83  46923  elaa2  46968  etransclem24  46992  etransclem32  47000  ioorrnopnlem  47038  issalnnd  47079  sge0xaddlem2  47168  sge0seq  47180  meaiininc2  47222  hoicvr  47282  ovnsubaddlem2  47305  hoidmvval0  47321  hoidmvlelem3  47331  hspmbllem2  47361  vonioo  47416  vonicc  47419  smfinflem  47551  fsupdm  47576  finfdm  47580  fmtnoprmfac2lem1  48338  fmtnofac1  48342  lincresunit3lem3  49274  suppdm  49310  inlinecirc02p  49587