Theorem 3adant1r 1196

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 487	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an1 1181	1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 1105

This theorem is referenced by:  mpof1o2d  8122  ecopovtrn  8819  isf32lem9  10346  axdc3lem4  10438  tskun  10772  dvdscmulr  16343  divalglem8  16459  ghmgrp  19133  dvfsumlem3  26168  dvfsumrlim  26171  dvfsumrlim2  26172  dvfsumrlim3  26173  dchrisumlem3  27636  dchrisum  27637  abvcxp  27760  padicabv  27775  hvmulcan  31405  isarchi2  33486  archiabllem2c  33496  hasheuni  34456  carsgclctunlem1  34688  carsggect  34689  carsgclctunlem2  34690  carsgclctunlem3  34691  carsgclctun  34692  carsgsiga  34693  omsmeas  34694  rankfilimbi  35476  pibt2  38044  tendoicl  41551  cdlemkfid2N  41678  erngdvlem4  41746  pellex  43545  refsumcn  45733  restuni3  45819  wessf1ornlem  45886  unirnmapsn  45913  ssmapsn  45915  iunmapsn  45916  ssfiunibd  46011  supxrgelem  46036  infleinf2  46111  fmuldfeq  46282  limsupmnfuzlem  46423  limsupre3uzlem  46432  cosknegpi  46566  icccncfext  46584  stoweidlem31  46728  stoweidlem43  46740  stoweidlem46  46743  stoweidlem52  46749  stoweidlem53  46750  stoweidlem54  46751  stoweidlem55  46752  stoweidlem56  46753  stoweidlem57  46754  stoweidlem58  46755  stoweidlem59  46756  stoweidlem60  46757  stoweidlem62  46759  stoweid  46760  fourierdlem12  46816  fourierdlem41  46845  fourierdlem48  46851  fourierdlem79  46882  fourierdlem81  46884  etransclem24  46955  etransclem46  46977  sge0f1o  47079  sge0iunmptlemre  47112  sge0iunmpt  47115  sge0seq  47143  caragenfiiuncl  47212  hoicvr  47245  hoidmvval0  47284  hspmbllem2  47324  smflimsuplem7  47523  el0ldep  49229  2arymaptfo  49417  itschlc0yqe  49523  itsclc0yqsol  49527