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  8744  isf32lem9  10252  axdc3lem4  10344  tskun  10677  dvdscmulr  16195  divalglem8  16311  ghmgrp  18979  dvfsumlem3  25962  dvfsumrlim  25965  dvfsumrlim2  25966  dvfsumrlim3  25967  dchrisumlem3  27429  dchrisum  27430  abvcxp  27553  padicabv  27568  hvmulcan  31052  isarchi2  33154  archiabllem2c  33164  hasheuni  34098  carsgclctunlem1  34330  carsggect  34331  carsgclctunlem2  34332  carsgclctunlem3  34333  carsgclctun  34334  carsgsiga  34335  omsmeas  34336  rankfilimbi  35112  pibt2  37461  tendoicl  40894  cdlemkfid2N  41021  erngdvlem4  41089  f1o2d2  42325  pellex  42927  refsumcn  45126  restuni3  45214  wessf1ornlem  45281  unirnmapsn  45310  ssmapsn  45312  iunmapsn  45313  ssfiunibd  45409  supxrgelem  45435  infleinf2  45511  fmuldfeq  45682  limsupmnfuzlem  45823  limsupre3uzlem  45832  cosknegpi  45966  icccncfext  45984  stoweidlem31  46128  stoweidlem43  46140  stoweidlem46  46143  stoweidlem52  46149  stoweidlem53  46150  stoweidlem54  46151  stoweidlem55  46152  stoweidlem56  46153  stoweidlem57  46154  stoweidlem58  46155  stoweidlem59  46156  stoweidlem60  46157  stoweidlem62  46159  stoweid  46160  fourierdlem12  46216  fourierdlem41  46245  fourierdlem48  46251  fourierdlem79  46282  fourierdlem81  46284  etransclem24  46355  etransclem46  46377  sge0f1o  46479  sge0iunmptlemre  46512  sge0iunmpt  46515  sge0seq  46543  caragenfiiuncl  46612  hoicvr  46645  hoidmvval0  46684  hspmbllem2  46724  smflimsuplem7  46923  el0ldep  48566  2arymaptfo  48754  itschlc0yqe  48860  itsclc0yqsol  48864