Theorem 3adant1r 1170

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 1156	1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  ecopovtrn  8250  isf32lem9  9629  axdc3lem4  9721  tskun  10054  dvdscmulr  15471  divalglem8  15584  ghmgrp  17980  dvfsumlem3  24308  dvfsumrlim  24311  dvfsumrlim2  24312  dvfsumrlim3  24313  dchrisumlem3  25749  dchrisum  25750  abvcxp  25873  padicabv  25888  hvmulcan  28540  isarchi2  30452  archiabllem2c  30462  hasheuni  30961  carsgclctunlem1  31192  carsggect  31193  carsgclctunlem2  31194  carsgclctunlem3  31195  carsgclctun  31196  carsgsiga  31197  omsmeas  31198  pibt2  34229  tendoicl  37463  cdlemkfid2N  37590  erngdvlem4  37658  pellex  38917  refsumcn  40826  restuni3  40924  wessf1ornlem  40985  unirnmapsn  41017  ssmapsn  41019  iunmapsn  41020  ssfiunibd  41117  supxrgelem  41146  infleinf2  41230  fmuldfeq  41406  limsupmnfuzlem  41549  limsupre3uzlem  41558  cosknegpi  41691  icccncfext  41711  stoweidlem31  41858  stoweidlem43  41870  stoweidlem46  41873  stoweidlem52  41879  stoweidlem53  41880  stoweidlem54  41881  stoweidlem55  41882  stoweidlem56  41883  stoweidlem57  41884  stoweidlem58  41885  stoweidlem59  41886  stoweidlem60  41887  stoweidlem62  41889  stoweid  41890  fourierdlem12  41946  fourierdlem41  41975  fourierdlem48  41981  fourierdlem79  42012  fourierdlem81  42014  etransclem24  42085  etransclem46  42107  sge0f1o  42206  sge0iunmptlemre  42239  sge0iunmpt  42242  sge0seq  42270  caragenfiiuncl  42339  hoicvr  42372  hoidmvval0  42411  hspmbllem2  42451  smflimsuplem7  42642  el0ldep  44001  itschlc0yqe  44228  itsclc0yqsol  44232