Theorem 3adant1r 1176

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 1162	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  ecopovtrn  8818  isf32lem9  10360  axdc3lem4  10452  tskun  10785  dvdscmulr  16233  divalglem8  16348  ghmgrp  18986  dvfsumlem3  25781  dvfsumrlim  25784  dvfsumrlim2  25785  dvfsumrlim3  25786  dchrisumlem3  27231  dchrisum  27232  abvcxp  27355  padicabv  27370  hvmulcan  30593  isarchi2  32602  archiabllem2c  32612  hasheuni  33382  carsgclctunlem1  33615  carsggect  33616  carsgclctunlem2  33617  carsgclctunlem3  33618  carsgclctun  33619  carsgsiga  33620  omsmeas  33621  pibt2  36602  tendoicl  39971  cdlemkfid2N  40098  erngdvlem4  40166  f1o2d2  41362  pellex  41876  refsumcn  44017  restuni3  44109  wessf1ornlem  44183  unirnmapsn  44212  ssmapsn  44214  iunmapsn  44215  ssfiunibd  44318  supxrgelem  44346  infleinf2  44423  fmuldfeq  44598  limsupmnfuzlem  44741  limsupre3uzlem  44750  cosknegpi  44884  icccncfext  44902  stoweidlem31  45046  stoweidlem43  45058  stoweidlem46  45061  stoweidlem52  45067  stoweidlem53  45068  stoweidlem54  45069  stoweidlem55  45070  stoweidlem56  45071  stoweidlem57  45072  stoweidlem58  45073  stoweidlem59  45074  stoweidlem60  45075  stoweidlem62  45077  stoweid  45078  fourierdlem12  45134  fourierdlem41  45163  fourierdlem48  45169  fourierdlem79  45200  fourierdlem81  45202  etransclem24  45273  etransclem46  45295  sge0f1o  45397  sge0iunmptlemre  45430  sge0iunmpt  45433  sge0seq  45461  caragenfiiuncl  45530  hoicvr  45563  hoidmvval0  45602  hspmbllem2  45642  smflimsuplem7  45841  el0ldep  47235  2arymaptfo  47428  itschlc0yqe  47534  itsclc0yqsol  47538