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  8126  ecopovtrn  8825  rankfilimbi  9883  isf32lem9  10420  axdc3lem4  10512  tskun  10852  dvdscmulr  16434  divalglem8  16550  ghmgrp  19256  dvfsumlem3  26328  dvfsumrlim  26331  dvfsumrlim2  26332  dvfsumrlim3  26333  dchrisumlem3  27800  dchrisum  27801  abvcxp  27924  padicabv  27939  hvmulcan  31656  isarchi2  33728  archiabllem2c  33738  hasheuni  34699  carsgclctunlem1  34932  carsggect  34933  carsgclctunlem2  34934  carsgclctunlem3  34935  carsgclctun  34936  carsgsiga  34937  omsmeas  34938  pibt2  38308  tendoicl  41821  cdlemkfid2N  41948  erngdvlem4  42016  pellex  43795  refsumcn  45990  restuni3  46076  wessf1ornlem  46143  unirnmapsn  46170  ssmapsn  46172  iunmapsn  46173  ssfiunibd  46268  supxrgelem  46293  infleinf2  46368  fmuldfeq  46539  limsupmnfuzlem  46680  limsupre3uzlem  46689  cosknegpi  46823  icccncfext  46841  stoweidlem31  46985  stoweidlem43  46997  stoweidlem46  47000  stoweidlem52  47006  stoweidlem53  47007  stoweidlem54  47008  stoweidlem55  47009  stoweidlem56  47010  stoweidlem57  47011  stoweidlem58  47012  stoweidlem59  47013  stoweidlem60  47014  stoweidlem62  47016  stoweid  47017  fourierdlem12  47073  fourierdlem41  47102  fourierdlem48  47108  fourierdlem79  47139  fourierdlem81  47141  etransclem24  47212  etransclem46  47234  sge0f1o  47336  sge0iunmptlemre  47369  sge0iunmpt  47372  sge0seq  47400  caragenfiiuncl  47469  hoicvr  47502  hoidmvval0  47541  hspmbllem2  47581  smflimsuplem7  47780  el0ldep  49522  2arymaptfo  49710  itschlc0yqe  49816  itsclc0yqsol  49820