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  8354  omeulem1  8566  f1oen4g  8960  f1dom4g  8961  dif1ennnALT  9236  ordiso2  9476  infpssrlem4  10289  fin1a2lem9  10391  gchpwdom  10654  tskwun  10768  gruxp  10791  infregelb  12198  fzo1fzo0n0  13743  fsuppmapnn0fiub  14026  pfxsuffeqwrdeq  14734  fprodle  16049  muldvds2  16338  dvds2add  16347  dvds2sub  16348  dvdstr  16351  lcmfledvds  16689  mndvcl  18854  mhmvlin  18858  mulgnnsubcl  19151  mulgpropd  19181  gexdvdsi  19652  ringidss  20359  reslmhm2  21151  obs2ss  21847  lsslindf  21948  issubassa  21985  madurid  22769  restntr  23307  cnpnei  23389  upxp  23748  qtopss  23840  opnfbas  23967  fbasrn  24009  trfg  24016  ufilmax  24032  ustuqtop1  24366  prdsxmetlem  24493  nmoix  24854  nmoi2  24855  iimulcl  25064  mbfimaopn2  25784  lgsval4lem  27437  nodenselem8  27820  f1otrg  29160  brbtwn2  29195  colinearalg  29200  axsegconlem1  29207  0vtxrusgr  29867  clwwlkccatlem  30280  clwwlkccat  30281  clwwisshclwws  30306  clwwlkfo  30341  numclwwlk1lem2fo  30649  lnosub  31051  pjspansn  31869  eulerpartlemb  34702  cnpconn  35620  mclspps  35974  curf  38136  mblfinlem2  38196  mblfinlem3  38197  mettrifi  38295  ghomdiv  38430  grpokerinj  38431  rngohomco  38512  crngohomfo  38544  keridl  38570  cvrcon3b  39940  mzpsubst  43370  lzunuz  43390  diophrex  43397  rmxycomplete  43535  jm2.26  43620  lnmepi  43703  lmhmlnmsplit  43705  nadd2rabex  44004  nadd1rabtr  44006  nadd1rabex  44008  ntrclsiso  44684  ntrclskb  44686  ntrclsk3  44687  uzwo4  45664  wessf1ornlem  45794  choicefi  45808  supxrgere  45940  supxrgelem  45944  supxrge  45945  suplesup  45946  infxr  45973  infleinflem2  45977  rexabslelem  46023  fmul01lt1  46193  limcleqr  46249  limclner  46256  dvnprodlem1  46551  volioc  46577  stoweidlem60  46665  wallispilem3  46672  fourierdlem12  46724  fourierdlem41  46753  fourierdlem42  46754  fourierdlem48  46759  fourierdlem49  46760  fourierdlem54  46765  fourierdlem68  46779  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem83  46794  elaa2  46839  etransclem24  46863  etransclem32  46871  ioorrnopnlem  46909  issalnnd  46950  sge0xaddlem2  47039  sge0seq  47051  meaiininc2  47093  hoicvr  47153  ovnsubaddlem2  47176  hoidmvval0  47192  hoidmvlelem3  47202  hspmbllem2  47232  vonioo  47287  vonicc  47290  smfinflem  47422  fsupdm  47447  finfdm  47451  fmtnoprmfac2lem1  48206  fmtnofac1  48210  lincresunit3lem3  49138  suppdm  49174  inlinecirc02p  49451