Theorem 3ad2antl1 1186

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 715	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1168	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

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

This theorem is referenced by:  simpl1  1192  simpl1l  1225  simpl1r  1226  simpl11  1249  simpl12  1250  simpl13  1251  smocdmdom  8298  omeulem1  8507  f1oen4g  8899  f1dom4g  8900  dif1ennnALT  9175  ordiso2  9418  infpssrlem4  10214  fin1a2lem9  10316  gchpwdom  10579  tskwun  10693  gruxp  10716  infregelb  12124  fzo1fzo0n0  13629  fsuppmapnn0fiub  13912  pfxsuffeqwrdeq  14619  fprodle  15917  muldvds2  16206  dvds2add  16215  dvds2sub  16216  dvdstr  16219  lcmfledvds  16557  mndvcl  18720  mhmvlin  18724  mulgnnsubcl  19014  mulgpropd  19044  gexdvdsi  19510  ringidss  20210  reslmhm2  21003  obs2ss  21682  lsslindf  21783  issubassa  21820  madurid  22586  restntr  23124  cnpnei  23206  upxp  23565  qtopss  23657  opnfbas  23784  fbasrn  23826  trfg  23833  ufilmax  23849  ustuqtop1  24183  prdsxmetlem  24310  nmoix  24671  nmoi2  24672  iimulcl  24887  mbfimaopn2  25612  lgsval4lem  27273  nodenselem8  27657  f1otrg  28892  brbtwn2  28927  colinearalg  28932  axsegconlem1  28939  0vtxrusgr  29600  clwwlkccatlem  30013  clwwlkccat  30014  clwwisshclwws  30039  clwwlkfo  30074  numclwwlk1lem2fo  30382  lnosub  30783  pjspansn  31601  eulerpartlemb  34474  cnpconn  35373  mclspps  35727  curf  37738  mblfinlem2  37798  mblfinlem3  37799  mettrifi  37897  ghomdiv  38032  grpokerinj  38033  rngohomco  38114  crngohomfo  38146  keridl  38172  cvrcon3b  39476  mzpsubst  42932  lzunuz  42952  diophrex  42959  rmxycomplete  43101  jm2.26  43186  lnmepi  43269  lmhmlnmsplit  43271  nadd2rabex  43570  nadd1rabtr  43572  nadd1rabex  43574  ntrclsiso  44250  ntrclskb  44252  ntrclsk3  44253  uzwo4  45240  wessf1ornlem  45371  choicefi  45386  supxrgere  45520  supxrgelem  45524  supxrge  45525  suplesup  45526  infxr  45553  infleinflem2  45557  rexabslelem  45604  fmul01lt1  45774  limcleqr  45830  limclner  45837  dvnprodlem1  46132  volioc  46158  stoweidlem60  46246  wallispilem3  46253  fourierdlem12  46305  fourierdlem41  46334  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem54  46346  fourierdlem68  46360  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem83  46375  elaa2  46420  etransclem24  46444  etransclem32  46452  ioorrnopnlem  46490  issalnnd  46531  sge0xaddlem2  46620  sge0seq  46632  meaiininc2  46674  hoicvr  46734  ovnsubaddlem2  46757  hoidmvval0  46773  hoidmvlelem3  46783  hspmbllem2  46813  vonioo  46868  vonicc  46871  smfinflem  47003  fsupdm  47028  finfdm  47032  fmtnoprmfac2lem1  47754  fmtnofac1  47758  lincresunit3lem3  48662  suppdm  48698  inlinecirc02p  48975