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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simpl1  1192  simpl1l  1225  simpl1r  1226  simpl11  1249  simpl12  1250  simpl13  1251  smocdmdom  8368  omeulem1  8582  f1oen4g  8960  f1dom4g  8961  dif1ennnALT  9277  ordiso2  9510  infpssrlem4  10301  fin1a2lem9  10403  gchpwdom  10665  tskwun  10779  gruxp  10802  infregelb  12198  fzo1fzo0n0  13683  fsuppmapnn0fiub  13956  pfxsuffeqwrdeq  14648  fprodle  15940  muldvds2  16225  dvds2add  16233  dvds2sub  16234  dvdstr  16237  lcmfledvds  16569  mulgnnsubcl  18966  mulgpropd  18996  gexdvdsi  19451  ringidss  20094  reslmhm2  20664  obs2ss  21284  lsslindf  21385  issubassa  21421  mndvcl  21893  mhmvlin  21899  madurid  22146  restntr  22686  cnpnei  22768  upxp  23127  qtopss  23219  opnfbas  23346  fbasrn  23388  trfg  23395  ufilmax  23411  ustuqtop1  23746  prdsxmetlem  23874  nmoix  24246  nmoi2  24247  iimulcl  24453  mbfimaopn2  25174  lgsval4lem  26811  nodenselem8  27194  f1otrg  28122  brbtwn2  28163  colinearalg  28168  axsegconlem1  28175  0vtxrusgr  28834  clwwlkccatlem  29242  clwwlkccat  29243  clwwisshclwws  29268  clwwlkfo  29303  numclwwlk1lem2fo  29611  lnosub  30012  pjspansn  30830  eulerpartlemb  33367  cnpconn  34221  mclspps  34575  curf  36466  mblfinlem2  36526  mblfinlem3  36527  mettrifi  36625  ghomdiv  36760  grpokerinj  36761  rngohomco  36842  crngohomfo  36874  keridl  36900  cvrcon3b  38147  factwoffsmonot  41023  mzpsubst  41486  lzunuz  41506  diophrex  41513  rmxycomplete  41656  jm2.26  41741  lnmepi  41827  lmhmlnmsplit  41829  nadd2rabex  42136  nadd1rabtr  42138  nadd1rabex  42140  ntrclsiso  42818  ntrclskb  42820  ntrclsk3  42821  uzwo4  43740  wessf1ornlem  43882  choicefi  43899  supxrgere  44043  supxrgelem  44047  supxrge  44048  suplesup  44049  infxr  44077  infleinflem2  44081  rexabslelem  44128  fmul01lt1  44302  limcleqr  44360  limclner  44367  dvnprodlem1  44662  volioc  44688  stoweidlem60  44776  wallispilem3  44783  fourierdlem12  44835  fourierdlem41  44864  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem54  44876  fourierdlem68  44890  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem83  44905  elaa2  44950  etransclem24  44974  etransclem32  44982  ioorrnopnlem  45020  issalnnd  45061  sge0xaddlem2  45150  sge0seq  45162  meaiininc2  45204  hoicvr  45264  ovnsubaddlem2  45287  hoidmvval0  45303  hoidmvlelem3  45313  hspmbllem2  45343  vonioo  45398  vonicc  45401  smfinflem  45533  fsupdm  45558  finfdm  45562  fmtnoprmfac2lem1  46234  fmtnofac1  46238  lincresunit3lem3  47155  suppdm  47191  inlinecirc02p  47473