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  8130  ecopovtrn  8827  isf32lem9  10363  axdc3lem4  10455  tskun  10789  dvdscmulr  16367  divalglem8  16483  ghmgrp  19163  dvfsumlem3  26224  dvfsumrlim  26227  dvfsumrlim2  26228  dvfsumrlim3  26229  dchrisumlem3  27692  dchrisum  27693  abvcxp  27816  padicabv  27831  hvmulcan  31461  isarchi2  33536  archiabllem2c  33546  hasheuni  34506  carsgclctunlem1  34739  carsggect  34740  carsgclctunlem2  34741  carsgclctunlem3  34742  carsgclctun  34743  carsgsiga  34744  omsmeas  34745  rankfilimbi  35520  pibt2  38104  tendoicl  41611  cdlemkfid2N  41738  erngdvlem4  41806  pellex  43603  refsumcn  45791  restuni3  45877  wessf1ornlem  45944  unirnmapsn  45971  ssmapsn  45973  iunmapsn  45974  ssfiunibd  46069  supxrgelem  46094  infleinf2  46169  fmuldfeq  46340  limsupmnfuzlem  46481  limsupre3uzlem  46490  cosknegpi  46624  icccncfext  46642  stoweidlem31  46786  stoweidlem43  46798  stoweidlem46  46801  stoweidlem52  46807  stoweidlem53  46808  stoweidlem54  46809  stoweidlem55  46810  stoweidlem56  46811  stoweidlem57  46812  stoweidlem58  46813  stoweidlem59  46814  stoweidlem60  46815  stoweidlem62  46817  stoweid  46818  fourierdlem12  46874  fourierdlem41  46903  fourierdlem48  46909  fourierdlem79  46940  fourierdlem81  46942  etransclem24  47013  etransclem46  47035  sge0f1o  47137  sge0iunmptlemre  47170  sge0iunmpt  47173  sge0seq  47201  caragenfiiuncl  47270  hoicvr  47303  hoidmvval0  47342  hspmbllem2  47382  smflimsuplem7  47581  el0ldep  49287  2arymaptfo  49475  itschlc0yqe  49581  itsclc0yqsol  49585