Theorem 3ad2antl1 1202

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 1184	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

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

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 1103

This theorem is referenced by:  simpl1  1208  simpl1l  1241  simpl1r  1242  simpl11  1265  simpl12  1266  simpl13  1267  smocdmdom  8355  omeulem1  8567  f1oen4g  8961  f1dom4g  8962  dif1ennnALT  9237  ordiso2  9477  infpssrlem4  10290  fin1a2lem9  10392  gchpwdom  10655  tskwun  10769  gruxp  10792  infregelb  12199  fzo1fzo0n0  13744  fsuppmapnn0fiub  14027  pfxsuffeqwrdeq  14735  fprodle  16050  muldvds2  16339  dvds2add  16348  dvds2sub  16349  dvdstr  16352  lcmfledvds  16690  mndvcl  18855  mhmvlin  18859  mulgnnsubcl  19152  mulgpropd  19182  gexdvdsi  19653  ringidss  20360  reslmhm2  21152  obs2ss  21848  lsslindf  21949  issubassa  21986  madurid  22770  restntr  23308  cnpnei  23390  upxp  23749  qtopss  23841  opnfbas  23968  fbasrn  24010  trfg  24017  ufilmax  24033  ustuqtop1  24367  prdsxmetlem  24494  nmoix  24855  nmoi2  24856  iimulcl  25065  mbfimaopn2  25785  lgsval4lem  27438  nodenselem8  27821  f1otrg  29161  brbtwn2  29196  colinearalg  29201  axsegconlem1  29208  0vtxrusgr  29868  clwwlkccatlem  30281  clwwlkccat  30282  clwwisshclwws  30307  clwwlkfo  30342  numclwwlk1lem2fo  30650  lnosub  31052  pjspansn  31870  eulerpartlemb  34703  cnpconn  35621  mclspps  35975  curf  38137  mblfinlem2  38197  mblfinlem3  38198  mettrifi  38296  ghomdiv  38431  grpokerinj  38432  rngohomco  38513  crngohomfo  38545  keridl  38571  cvrcon3b  39941  mzpsubst  43371  lzunuz  43391  diophrex  43398  rmxycomplete  43536  jm2.26  43621  lnmepi  43704  lmhmlnmsplit  43706  nadd2rabex  44005  nadd1rabtr  44007  nadd1rabex  44009  ntrclsiso  44685  ntrclskb  44687  ntrclsk3  44688  uzwo4  45665  wessf1ornlem  45795  choicefi  45809  supxrgere  45941  supxrgelem  45945  supxrge  45946  suplesup  45947  infxr  45974  infleinflem2  45978  rexabslelem  46024  fmul01lt1  46194  limcleqr  46250  limclner  46257  dvnprodlem1  46552  volioc  46578  stoweidlem60  46666  wallispilem3  46673  fourierdlem12  46725  fourierdlem41  46754  fourierdlem42  46755  fourierdlem48  46760  fourierdlem49  46761  fourierdlem54  46766  fourierdlem68  46780  fourierdlem73  46785  fourierdlem74  46786  fourierdlem75  46787  fourierdlem83  46795  elaa2  46840  etransclem24  46864  etransclem32  46872  ioorrnopnlem  46910  issalnnd  46951  sge0xaddlem2  47040  sge0seq  47052  meaiininc2  47094  hoicvr  47154  ovnsubaddlem2  47177  hoidmvval0  47193  hoidmvlelem3  47203  hspmbllem2  47233  vonioo  47288  vonicc  47291  smfinflem  47423  fsupdm  47448  finfdm  47452  fmtnoprmfac2lem1  48207  fmtnofac1  48211  lincresunit3lem3  49139  suppdm  49175  inlinecirc02p  49452