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  8127  ecopovtrn  8824  isf32lem9  10367  axdc3lem4  10459  tskun  10799  dvdscmulr  16380  divalglem8  16496  ghmgrp  19195  dvfsumlem3  26262  dvfsumrlim  26265  dvfsumrlim2  26266  dvfsumrlim3  26267  dchrisumlem3  27735  dchrisum  27736  abvcxp  27859  padicabv  27874  hvmulcan  31561  isarchi2  33633  archiabllem2c  33643  hasheuni  34603  carsgclctunlem1  34836  carsggect  34837  carsgclctunlem2  34838  carsgclctunlem3  34839  carsgclctun  34840  carsgsiga  34841  omsmeas  34842  rankfilimbi  35617  pibt2  38179  tendoicl  41677  cdlemkfid2N  41804  erngdvlem4  41872  pellex  43684  refsumcn  45872  restuni3  45958  wessf1ornlem  46025  unirnmapsn  46052  ssmapsn  46054  iunmapsn  46055  ssfiunibd  46150  supxrgelem  46175  infleinf2  46250  fmuldfeq  46421  limsupmnfuzlem  46562  limsupre3uzlem  46571  cosknegpi  46705  icccncfext  46723  stoweidlem31  46867  stoweidlem43  46879  stoweidlem46  46882  stoweidlem52  46888  stoweidlem53  46889  stoweidlem54  46890  stoweidlem55  46891  stoweidlem56  46892  stoweidlem57  46893  stoweidlem58  46894  stoweidlem59  46895  stoweidlem60  46896  stoweidlem62  46898  stoweid  46899  fourierdlem12  46955  fourierdlem41  46984  fourierdlem48  46990  fourierdlem79  47021  fourierdlem81  47023  etransclem24  47094  etransclem46  47116  sge0f1o  47218  sge0iunmptlemre  47251  sge0iunmpt  47254  sge0seq  47282  caragenfiiuncl  47351  hoicvr  47384  hoidmvval0  47423  hspmbllem2  47463  smflimsuplem7  47662  el0ldep  49404  2arymaptfo  49592  itschlc0yqe  49698  itsclc0yqsol  49702