Theorem 3ad2antl1 1192

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpl1  1198  simpl1l  1231  simpl1r  1232  simpl11  1255  simpl12  1256  simpl13  1257  smocdmdom  8298  omeulem1  8507  f1oen4g  8901  f1dom4g  8902  dif1ennnALT  9177  ordiso2  9420  infpssrlem4  10219  fin1a2lem9  10321  gchpwdom  10584  tskwun  10698  gruxp  10721  infregelb  12131  fzo1fzo0n0  13661  fsuppmapnn0fiub  13944  pfxsuffeqwrdeq  14651  fprodle  15952  muldvds2  16241  dvds2add  16250  dvds2sub  16251  dvdstr  16254  lcmfledvds  16592  mndvcl  18756  mhmvlin  18760  mulgnnsubcl  19053  mulgpropd  19083  gexdvdsi  19549  ringidss  20249  reslmhm2  21043  obs2ss  21704  lsslindf  21805  issubassa  21842  madurid  22627  restntr  23165  cnpnei  23247  upxp  23606  qtopss  23698  opnfbas  23825  fbasrn  23867  trfg  23874  ufilmax  23890  ustuqtop1  24224  prdsxmetlem  24351  nmoix  24712  nmoi2  24713  iimulcl  24922  mbfimaopn2  25642  lgsval4lem  27289  nodenselem8  27673  f1otrg  28957  brbtwn2  28992  colinearalg  28997  axsegconlem1  29004  0vtxrusgr  29664  clwwlkccatlem  30077  clwwlkccat  30078  clwwisshclwws  30103  clwwlkfo  30138  numclwwlk1lem2fo  30446  lnosub  30848  pjspansn  31666  eulerpartlemb  34552  cnpconn  35458  mclspps  35812  curf  37965  mblfinlem2  38025  mblfinlem3  38026  mettrifi  38124  ghomdiv  38259  grpokerinj  38260  rngohomco  38341  crngohomfo  38373  keridl  38399  cvrcon3b  39769  mzpsubst  43197  lzunuz  43217  diophrex  43224  rmxycomplete  43362  jm2.26  43447  lnmepi  43530  lmhmlnmsplit  43532  nadd2rabex  43831  nadd1rabtr  43833  nadd1rabex  43835  ntrclsiso  44511  ntrclskb  44513  ntrclsk3  44514  uzwo4  45501  wessf1ornlem  45632  choicefi  45646  supxrgere  45778  supxrgelem  45782  supxrge  45783  suplesup  45784  infxr  45811  infleinflem2  45815  rexabslelem  45861  fmul01lt1  46031  limcleqr  46087  limclner  46094  dvnprodlem1  46389  volioc  46415  stoweidlem60  46503  wallispilem3  46510  fourierdlem12  46562  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fourierdlem49  46598  fourierdlem54  46603  fourierdlem68  46617  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem83  46632  elaa2  46677  etransclem24  46701  etransclem32  46709  ioorrnopnlem  46747  issalnnd  46788  sge0xaddlem2  46877  sge0seq  46889  meaiininc2  46931  hoicvr  46991  ovnsubaddlem2  47014  hoidmvval0  47030  hoidmvlelem3  47040  hspmbllem2  47070  vonioo  47125  vonicc  47128  smfinflem  47260  fsupdm  47285  finfdm  47289  fmtnoprmfac2lem1  48044  fmtnofac1  48048  lincresunit3lem3  48965  suppdm  49001  inlinecirc02p  49278