Theorem 3adant1r 1179

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ecopovtrn  8760  isf32lem9  10274  axdc3lem4  10366  tskun  10700  dvdscmulr  16244  divalglem8  16360  ghmgrp  19033  dvfsumlem3  26005  dvfsumrlim  26008  dvfsumrlim2  26009  dvfsumrlim3  26010  dchrisumlem3  27468  dchrisum  27469  abvcxp  27592  padicabv  27607  hvmulcan  31158  isarchi2  33261  archiabllem2c  33271  hasheuni  34245  carsgclctunlem1  34477  carsggect  34478  carsgclctunlem2  34479  carsgclctunlem3  34480  carsgclctun  34481  carsgsiga  34482  omsmeas  34483  rankfilimbi  35260  pibt2  37747  tendoicl  41256  cdlemkfid2N  41383  erngdvlem4  41451  f1o2d2  42688  pellex  43281  refsumcn  45479  restuni3  45566  wessf1ornlem  45633  unirnmapsn  45661  ssmapsn  45663  iunmapsn  45664  ssfiunibd  45760  supxrgelem  45785  infleinf2  45860  fmuldfeq  46031  limsupmnfuzlem  46172  limsupre3uzlem  46181  cosknegpi  46315  icccncfext  46333  stoweidlem31  46477  stoweidlem43  46489  stoweidlem46  46492  stoweidlem52  46498  stoweidlem53  46499  stoweidlem54  46500  stoweidlem55  46501  stoweidlem56  46502  stoweidlem57  46503  stoweidlem58  46504  stoweidlem59  46505  stoweidlem60  46506  stoweidlem62  46508  stoweid  46509  fourierdlem12  46565  fourierdlem41  46594  fourierdlem48  46600  fourierdlem79  46631  fourierdlem81  46633  etransclem24  46704  etransclem46  46726  sge0f1o  46828  sge0iunmptlemre  46861  sge0iunmpt  46864  sge0seq  46892  caragenfiiuncl  46961  hoicvr  46994  hoidmvval0  47033  hspmbllem2  47073  smflimsuplem7  47272  el0ldep  48954  2arymaptfo  49142  itschlc0yqe  49248  itsclc0yqsol  49252