Theorem 3adant1r 1179

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant1r	⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant1r

Step	Hyp	Ref	Expression
1		simpl 486	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an1 1165	1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  ecopovtrn  8480  isf32lem9  9940  axdc3lem4  10032  tskun  10365  dvdscmulr  15809  divalglem8  15924  ghmgrp  18441  dvfsumlem3  24879  dvfsumrlim  24882  dvfsumrlim2  24883  dvfsumrlim3  24884  dchrisumlem3  26326  dchrisum  26327  abvcxp  26450  padicabv  26465  hvmulcan  29107  isarchi2  31112  archiabllem2c  31122  hasheuni  31719  carsgclctunlem1  31950  carsggect  31951  carsgclctunlem2  31952  carsgclctunlem3  31953  carsgclctun  31954  carsgsiga  31955  omsmeas  31956  pibt2  35274  tendoicl  38496  cdlemkfid2N  38623  erngdvlem4  38691  pellex  40301  refsumcn  42187  restuni3  42281  wessf1ornlem  42336  unirnmapsn  42368  ssmapsn  42370  iunmapsn  42371  ssfiunibd  42462  supxrgelem  42490  infleinf2  42568  fmuldfeq  42742  limsupmnfuzlem  42885  limsupre3uzlem  42894  cosknegpi  43028  icccncfext  43046  stoweidlem31  43190  stoweidlem43  43202  stoweidlem46  43205  stoweidlem52  43211  stoweidlem53  43212  stoweidlem54  43213  stoweidlem55  43214  stoweidlem56  43215  stoweidlem57  43216  stoweidlem58  43217  stoweidlem59  43218  stoweidlem60  43219  stoweidlem62  43221  stoweid  43222  fourierdlem12  43278  fourierdlem41  43307  fourierdlem48  43313  fourierdlem79  43344  fourierdlem81  43346  etransclem24  43417  etransclem46  43439  sge0f1o  43538  sge0iunmptlemre  43571  sge0iunmpt  43574  sge0seq  43602  caragenfiiuncl  43671  hoicvr  43704  hoidmvval0  43743  hspmbllem2  43783  smflimsuplem7  43974  el0ldep  45423  2arymaptfo  45616  itschlc0yqe  45722  itsclc0yqsol  45726