Theorem 3ad2antl1 1216

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  smorndom  7352  omeulem1  7549  dif1en  8078  ordiso2  8303  infpssrlem4  9011  fin1a2lem9  9113  gchpwdom  9371  tskwun  9485  gruxp  9508  infregelb  10884  fzo1fzo0n0  12386  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  fprodle  14566  muldvds2  14845  dvds2add  14853  dvds2sub  14854  dvdstr  14856  lcmfledvds  15183  mulgnnsubcl  17376  mulgpropd  17407  gexdvdsi  17821  ringidss  18400  reslmhm2  18874  issubassa  19145  obs2ss  19892  lsslindf  19988  mndvcl  20016  mhmvlin  20022  madurid  20269  restntr  20796  cnpnei  20878  upxp  21236  qtopss  21328  opnfbas  21456  fbasrn  21498  trfg  21505  ufilmax  21521  ustuqtop1  21855  prdsxmetlem  21983  nmoix  22343  nmoi2  22344  iimulcl  22544  mbfimaopn2  23230  lgsval4lem  24833  f1otrg  25551  brbtwn2  25585  colinearalg  25590  axsegconlem1  25597  redwlk  26136  vdn1frgrav2  26552  usg2spot2nb  26592  numclwlk1lem2fo  26622  lnosub  26998  pjspansn  27820  eulerpartlemb  29757  cnpcon  30466  mclspps  30735  nodenselem8  31087  curf  32557  mblfinlem2  32617  mblfinlem3  32618  mettrifi  32723  ghomdiv  32861  grpokerinj  32862  rngohomco  32943  crngohomfo  32975  keridl  33001  cvrcon3b  33582  mzpsubst  36329  lzunuz  36349  diophrex  36357  rmxycomplete  36500  jm2.26  36587  lnmepi  36673  lmhmlnmsplit  36675  ntrclsiso  37385  ntrclskb  37387  ntrclsk3  37388  uzwo4  38246  wessf1ornlem  38366  choicefi  38387  supxrgere  38490  supxrgelem  38494  supxrge  38495  suplesup  38496  infxr  38524  infleinflem2  38528  fmul01lt1  38653  limcleqr  38711  limclner  38718  dvnprodlem1  38836  volioc  38864  stoweidlem60  38953  wallispilem3  38960  fourierdlem12  39012  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem54  39053  fourierdlem68  39067  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem83  39082  elaa2  39127  etransclem24  39151  etransclem32  39159  ioorrnopnlem  39200  issalnnd  39239  sge0xaddlem2  39327  sge0seq  39339  meaiininc2  39378  hoicvr  39438  ovnsubaddlem2  39461  hoidmvval0  39477  hoidmvlelem3  39487  hspmbllem2  39517  vonioo  39573  vonicc  39576  fmtnoprmfac2lem1  40016  fmtnofac1  40020  0vtxrusgr  40777  clwwlksfo  41225  clwwisshclwws  41235  av-extwwlkfablem2  41510  av-numclwlk1lem2fo  41525  lincresunit3lem3  42057  suppdm  42094