Theorem 3adant1r 1177

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  ecopovtrn  8766  isf32lem9  10306  axdc3lem4  10398  tskun  10731  dvdscmulr  16178  divalglem8  16293  ghmgrp  18885  dvfsumlem3  25429  dvfsumrlim  25432  dvfsumrlim2  25433  dvfsumrlim3  25434  dchrisumlem3  26876  dchrisum  26877  abvcxp  27000  padicabv  27015  hvmulcan  30077  isarchi2  32091  archiabllem2c  32101  hasheuni  32773  carsgclctunlem1  33006  carsggect  33007  carsgclctunlem2  33008  carsgclctunlem3  33009  carsgclctun  33010  carsgsiga  33011  omsmeas  33012  pibt2  35961  tendoicl  39332  cdlemkfid2N  39459  erngdvlem4  39527  pellex  41216  refsumcn  43357  restuni3  43450  wessf1ornlem  43525  unirnmapsn  43556  ssmapsn  43558  iunmapsn  43559  ssfiunibd  43664  supxrgelem  43692  infleinf2  43769  fmuldfeq  43944  limsupmnfuzlem  44087  limsupre3uzlem  44096  cosknegpi  44230  icccncfext  44248  stoweidlem31  44392  stoweidlem43  44404  stoweidlem46  44407  stoweidlem52  44413  stoweidlem53  44414  stoweidlem54  44415  stoweidlem55  44416  stoweidlem56  44417  stoweidlem57  44418  stoweidlem58  44419  stoweidlem59  44420  stoweidlem60  44421  stoweidlem62  44423  stoweid  44424  fourierdlem12  44480  fourierdlem41  44509  fourierdlem48  44515  fourierdlem79  44546  fourierdlem81  44548  etransclem24  44619  etransclem46  44641  sge0f1o  44743  sge0iunmptlemre  44776  sge0iunmpt  44779  sge0seq  44807  caragenfiiuncl  44876  hoicvr  44909  hoidmvval0  44948  hspmbllem2  44988  smflimsuplem7  45187  el0ldep  46667  2arymaptfo  46860  itschlc0yqe  46966  itsclc0yqsol  46970