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 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  simpl1  1189  simpl1l  1222  simpl1r  1223  simpl11  1246  simpl12  1247  simpl13  1248  smocdmdom  8370  omeulem1  8584  f1oen4g  8962  f1dom4g  8963  dif1ennnALT  9279  ordiso2  9512  infpssrlem4  10303  fin1a2lem9  10405  gchpwdom  10667  tskwun  10781  gruxp  10804  infregelb  12202  fzo1fzo0n0  13687  fsuppmapnn0fiub  13960  pfxsuffeqwrdeq  14652  fprodle  15944  muldvds2  16229  dvds2add  16237  dvds2sub  16238  dvdstr  16241  lcmfledvds  16573  mulgnnsubcl  19002  mulgpropd  19032  gexdvdsi  19492  ringidss  20165  reslmhm2  20808  obs2ss  21503  lsslindf  21604  issubassa  21640  mndvcl  22113  mhmvlin  22119  madurid  22366  restntr  22906  cnpnei  22988  upxp  23347  qtopss  23439  opnfbas  23566  fbasrn  23608  trfg  23615  ufilmax  23631  ustuqtop1  23966  prdsxmetlem  24094  nmoix  24466  nmoi2  24467  iimulcl  24680  mbfimaopn2  25406  lgsval4lem  27047  nodenselem8  27430  f1otrg  28389  brbtwn2  28430  colinearalg  28435  axsegconlem1  28442  0vtxrusgr  29101  clwwlkccatlem  29509  clwwlkccat  29510  clwwisshclwws  29535  clwwlkfo  29570  numclwwlk1lem2fo  29878  lnosub  30279  pjspansn  31097  eulerpartlemb  33665  cnpconn  34519  mclspps  34873  curf  36769  mblfinlem2  36829  mblfinlem3  36830  mettrifi  36928  ghomdiv  37063  grpokerinj  37064  rngohomco  37145  crngohomfo  37177  keridl  37203  cvrcon3b  38450  factwoffsmonot  41329  mzpsubst  41788  lzunuz  41808  diophrex  41815  rmxycomplete  41958  jm2.26  42043  lnmepi  42129  lmhmlnmsplit  42131  nadd2rabex  42438  nadd1rabtr  42440  nadd1rabex  42442  ntrclsiso  43120  ntrclskb  43122  ntrclsk3  43123  uzwo4  44041  wessf1ornlem  44182  choicefi  44197  supxrgere  44341  supxrgelem  44345  supxrge  44346  suplesup  44347  infxr  44375  infleinflem2  44379  rexabslelem  44426  fmul01lt1  44600  limcleqr  44658  limclner  44665  dvnprodlem1  44960  volioc  44986  stoweidlem60  45074  wallispilem3  45081  fourierdlem12  45133  fourierdlem41  45162  fourierdlem42  45163  fourierdlem48  45168  fourierdlem49  45169  fourierdlem54  45174  fourierdlem68  45188  fourierdlem73  45193  fourierdlem74  45194  fourierdlem75  45195  fourierdlem83  45203  elaa2  45248  etransclem24  45272  etransclem32  45280  ioorrnopnlem  45318  issalnnd  45359  sge0xaddlem2  45448  sge0seq  45460  meaiininc2  45502  hoicvr  45562  ovnsubaddlem2  45585  hoidmvval0  45601  hoidmvlelem3  45611  hspmbllem2  45641  vonioo  45696  vonicc  45699  smfinflem  45831  fsupdm  45856  finfdm  45860  fmtnoprmfac2lem1  46532  fmtnofac1  46536  lincresunit3lem3  47242  suppdm  47278  inlinecirc02p  47560