Theorem 3adant1r 1190

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 1175	1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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

This theorem is referenced by:  mpof1o2d  8098  ecopovtrn  8795  isf32lem9  10311  axdc3lem4  10403  tskun  10737  dvdscmulr  16308  divalglem8  16424  ghmgrp  19098  dvfsumlem3  26077  dvfsumrlim  26080  dvfsumrlim2  26081  dvfsumrlim3  26082  dchrisumlem3  27542  dchrisum  27543  abvcxp  27666  padicabv  27681  hvmulcan  31231  isarchi2  33325  archiabllem2c  33335  hasheuni  34342  carsgclctunlem1  34574  carsggect  34575  carsgclctunlem2  34576  carsgclctunlem3  34577  carsgclctun  34578  carsgsiga  34579  omsmeas  34580  rankfilimbi  35357  pibt2  37871  tendoicl  41380  cdlemkfid2N  41507  erngdvlem4  41575  pellex  43372  refsumcn  45570  restuni3  45656  wessf1ornlem  45723  unirnmapsn  45750  ssmapsn  45752  iunmapsn  45753  ssfiunibd  45848  supxrgelem  45873  infleinf2  45948  fmuldfeq  46119  limsupmnfuzlem  46260  limsupre3uzlem  46269  cosknegpi  46403  icccncfext  46421  stoweidlem31  46565  stoweidlem43  46577  stoweidlem46  46580  stoweidlem52  46586  stoweidlem53  46587  stoweidlem54  46588  stoweidlem55  46589  stoweidlem56  46590  stoweidlem57  46591  stoweidlem58  46592  stoweidlem59  46593  stoweidlem60  46594  stoweidlem62  46596  stoweid  46597  fourierdlem12  46653  fourierdlem41  46682  fourierdlem48  46688  fourierdlem79  46719  fourierdlem81  46721  etransclem24  46792  etransclem46  46814  sge0f1o  46916  sge0iunmptlemre  46949  sge0iunmpt  46952  sge0seq  46980  caragenfiiuncl  47049  hoicvr  47082  hoidmvval0  47121  hspmbllem2  47161  smflimsuplem7  47360  el0ldep  49048  2arymaptfo  49236  itschlc0yqe  49342  itsclc0yqsol  49346