Theorem 3ad2antl1 1183

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simpl1  1189  simpl1l  1222  simpl1r  1223  simpl11  1246  simpl12  1247  simpl13  1248  smorndom  8170  omeulem1  8375  dif1enALT  8980  ordiso2  9204  infpssrlem4  9993  fin1a2lem9  10095  gchpwdom  10357  tskwun  10471  gruxp  10494  infregelb  11889  fzo1fzo0n0  13366  fsuppmapnn0fiub  13639  ccat2s1fvwOLD  14278  pfxsuffeqwrdeq  14339  fprodle  15634  muldvds2  15919  dvds2add  15927  dvds2sub  15928  dvdstr  15931  lcmfledvds  16265  mulgnnsubcl  18631  mulgpropd  18660  gexdvdsi  19103  ringidss  19731  reslmhm2  20230  obs2ss  20846  lsslindf  20947  issubassa  20983  mndvcl  21450  mhmvlin  21456  madurid  21701  restntr  22241  cnpnei  22323  upxp  22682  qtopss  22774  opnfbas  22901  fbasrn  22943  trfg  22950  ufilmax  22966  ustuqtop1  23301  prdsxmetlem  23429  nmoix  23799  nmoi2  23800  iimulcl  24006  mbfimaopn2  24726  lgsval4lem  26361  f1otrg  27136  brbtwn2  27176  colinearalg  27181  axsegconlem1  27188  0vtxrusgr  27847  clwwlkccatlem  28254  clwwlkccat  28255  clwwisshclwws  28280  clwwlkfo  28315  numclwwlk1lem2fo  28623  lnosub  29022  pjspansn  29840  eulerpartlemb  32235  cnpconn  33092  mclspps  33446  nodenselem8  33821  curf  35682  mblfinlem2  35742  mblfinlem3  35743  mettrifi  35842  ghomdiv  35977  grpokerinj  35978  rngohomco  36059  crngohomfo  36091  keridl  36117  cvrcon3b  37218  factwoffsmonot  40091  mzpsubst  40486  lzunuz  40506  diophrex  40513  rmxycomplete  40655  jm2.26  40740  lnmepi  40826  lmhmlnmsplit  40828  ntrclsiso  41566  ntrclskb  41568  ntrclsk3  41569  uzwo4  42490  wessf1ornlem  42611  choicefi  42629  supxrgere  42762  supxrgelem  42766  supxrge  42767  suplesup  42768  infxr  42796  infleinflem2  42800  rexabslelem  42848  fmul01lt1  43017  limcleqr  43075  limclner  43082  dvnprodlem1  43377  volioc  43403  stoweidlem60  43491  wallispilem3  43498  fourierdlem12  43550  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem54  43591  fourierdlem68  43605  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem83  43620  elaa2  43665  etransclem24  43689  etransclem32  43697  ioorrnopnlem  43735  issalnnd  43774  sge0xaddlem2  43862  sge0seq  43874  meaiininc2  43916  hoicvr  43976  ovnsubaddlem2  43999  hoidmvval0  44015  hoidmvlelem3  44025  hspmbllem2  44055  vonioo  44110  vonicc  44113  smfinflem  44237  fmtnoprmfac2lem1  44906  fmtnofac1  44910  lincresunit3lem3  45703  suppdm  45739  inlinecirc02p  46021