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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mpof1o2d  8167  ecopovtrn  8872  rankfilimbi  9932  isf32lem9  10469  axdc3lem4  10561  tskun  10901  dvdscmulr  16486  divalglem8  16602  ghmgrp  19308  dvfsumlem3  26381  dvfsumrlim  26384  dvfsumrlim2  26385  dvfsumrlim3  26386  dchrisumlem3  27851  dchrisum  27852  abvcxp  27975  padicabv  27990  hvmulcan  31707  isarchi2  33822  archiabllem2c  33832  hasheuni  34800  carsgclctunlem1  35032  carsggect  35033  carsgclctunlem2  35034  carsgclctunlem3  35035  carsgclctun  35036  carsgsiga  35037  omsmeas  35038  pibt2  38545  tendoicl  42056  cdlemkfid2N  42183  erngdvlem4  42251  pellex  44046  refsumcn  46263  restuni3  46348  wessf1ornlem  46415  unirnmapsn  46442  ssmapsn  46444  iunmapsn  46445  ssfiunibd  46540  supxrgelem  46564  infleinf2  46639  fmuldfeq  46810  limsupmnfuzlem  46951  limsupre3uzlem  46960  cosknegpi  47094  icccncfext  47112  stoweidlem31  47256  stoweidlem43  47268  stoweidlem46  47271  stoweidlem52  47277  stoweidlem53  47278  stoweidlem54  47279  stoweidlem55  47280  stoweidlem56  47281  stoweidlem57  47282  stoweidlem58  47283  stoweidlem59  47284  stoweidlem60  47285  stoweidlem62  47287  stoweid  47288  fourierdlem12  47344  fourierdlem41  47373  fourierdlem48  47379  fourierdlem79  47410  fourierdlem81  47412  etransclem24  47483  etransclem46  47505  sge0f1o  47607  sge0iunmptlemre  47640  sge0iunmpt  47643  sge0seq  47671  caragenfiiuncl  47740  hoicvr  47773  hoidmvval0  47812  hspmbllem2  47852  smflimsuplem7  48051  el0ldep  49793  2arymaptfo  49981  itschlc0yqe  50087  itsclc0yqsol  50091