Theorem 3adant1r 1184

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

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

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 1094

This theorem is referenced by:  mpof1o2d  8072  ecopovtrn  8764  isf32lem9  10281  axdc3lem4  10373  tskun  10707  dvdscmulr  16251  divalglem8  16367  ghmgrp  19040  dvfsumlem3  26020  dvfsumrlim  26023  dvfsumrlim2  26024  dvfsumrlim3  26025  dchrisumlem3  27479  dchrisum  27480  abvcxp  27603  padicabv  27618  hvmulcan  31168  isarchi2  33273  archiabllem2c  33283  hasheuni  34276  carsgclctunlem1  34508  carsggect  34509  carsgclctunlem2  34510  carsgclctunlem3  34511  carsgclctun  34512  carsgsiga  34513  omsmeas  34514  rankfilimbi  35289  pibt2  37786  tendoicl  41295  cdlemkfid2N  41422  erngdvlem4  41490  pellex  43287  refsumcn  45485  restuni3  45572  wessf1ornlem  45639  unirnmapsn  45666  ssmapsn  45668  iunmapsn  45669  ssfiunibd  45764  supxrgelem  45789  infleinf2  45864  fmuldfeq  46035  limsupmnfuzlem  46176  limsupre3uzlem  46185  cosknegpi  46319  icccncfext  46337  stoweidlem31  46481  stoweidlem43  46493  stoweidlem46  46496  stoweidlem52  46502  stoweidlem53  46503  stoweidlem54  46504  stoweidlem55  46505  stoweidlem56  46506  stoweidlem57  46507  stoweidlem58  46508  stoweidlem59  46509  stoweidlem60  46510  stoweidlem62  46512  stoweid  46513  fourierdlem12  46569  fourierdlem41  46598  fourierdlem48  46604  fourierdlem79  46635  fourierdlem81  46637  etransclem24  46708  etransclem46  46730  sge0f1o  46832  sge0iunmptlemre  46865  sge0iunmpt  46868  sge0seq  46896  caragenfiiuncl  46965  hoicvr  46998  hoidmvval0  47037  hspmbllem2  47077  smflimsuplem7  47276  el0ldep  48964  2arymaptfo  49152  itschlc0yqe  49258  itsclc0yqsol  49262