Theorem 3adant1r 1178

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ecopovtrn  8793  isf32lem9  10314  axdc3lem4  10406  tskun  10739  dvdscmulr  16254  divalglem8  16370  ghmgrp  18998  dvfsumlem3  25935  dvfsumrlim  25938  dvfsumrlim2  25939  dvfsumrlim3  25940  dchrisumlem3  27402  dchrisum  27403  abvcxp  27526  padicabv  27541  hvmulcan  31001  isarchi2  33139  archiabllem2c  33149  hasheuni  34075  carsgclctunlem1  34308  carsggect  34309  carsgclctunlem2  34310  carsgclctunlem3  34311  carsgclctun  34312  carsgsiga  34313  omsmeas  34314  pibt2  37405  tendoicl  40790  cdlemkfid2N  40917  erngdvlem4  40985  f1o2d2  42221  pellex  42823  refsumcn  45024  restuni3  45112  wessf1ornlem  45179  unirnmapsn  45208  ssmapsn  45210  iunmapsn  45211  ssfiunibd  45307  supxrgelem  45333  infleinf2  45410  fmuldfeq  45581  limsupmnfuzlem  45724  limsupre3uzlem  45733  cosknegpi  45867  icccncfext  45885  stoweidlem31  46029  stoweidlem43  46041  stoweidlem46  46044  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  stoweidlem55  46053  stoweidlem56  46054  stoweidlem57  46055  stoweidlem58  46056  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  stoweid  46061  fourierdlem12  46117  fourierdlem41  46146  fourierdlem48  46152  fourierdlem79  46183  fourierdlem81  46185  etransclem24  46256  etransclem46  46278  sge0f1o  46380  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0seq  46444  caragenfiiuncl  46513  hoicvr  46546  hoidmvval0  46585  hspmbllem2  46625  smflimsuplem7  46824  el0ldep  48455  2arymaptfo  48643  itschlc0yqe  48749  itsclc0yqsol  48753