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  8752  isf32lem9  10261  axdc3lem4  10353  tskun  10686  dvdscmulr  16199  divalglem8  16315  ghmgrp  18983  dvfsumlem3  25965  dvfsumrlim  25968  dvfsumrlim2  25969  dvfsumrlim3  25970  dchrisumlem3  27432  dchrisum  27433  abvcxp  27556  padicabv  27571  hvmulcan  31056  isarchi2  33163  archiabllem2c  33173  hasheuni  34121  carsgclctunlem1  34353  carsggect  34354  carsgclctunlem2  34355  carsgclctunlem3  34356  carsgclctun  34357  carsgsiga  34358  omsmeas  34359  rankfilimbi  35135  pibt2  37484  tendoicl  40918  cdlemkfid2N  41045  erngdvlem4  41113  f1o2d2  42354  pellex  42955  refsumcn  45154  restuni3  45242  wessf1ornlem  45309  unirnmapsn  45338  ssmapsn  45340  iunmapsn  45341  ssfiunibd  45437  supxrgelem  45463  infleinf2  45539  fmuldfeq  45710  limsupmnfuzlem  45851  limsupre3uzlem  45860  cosknegpi  45994  icccncfext  46012  stoweidlem31  46156  stoweidlem43  46168  stoweidlem46  46171  stoweidlem52  46177  stoweidlem53  46178  stoweidlem54  46179  stoweidlem55  46180  stoweidlem56  46181  stoweidlem57  46182  stoweidlem58  46183  stoweidlem59  46184  stoweidlem60  46185  stoweidlem62  46187  stoweid  46188  fourierdlem12  46244  fourierdlem41  46273  fourierdlem48  46279  fourierdlem79  46310  fourierdlem81  46312  etransclem24  46383  etransclem46  46405  sge0f1o  46507  sge0iunmptlemre  46540  sge0iunmpt  46543  sge0seq  46571  caragenfiiuncl  46640  hoicvr  46673  hoidmvval0  46712  hspmbllem2  46752  smflimsuplem7  46951  el0ldep  48594  2arymaptfo  48782  itschlc0yqe  48888  itsclc0yqsol  48892