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  8834  isf32lem9  10375  axdc3lem4  10467  tskun  10800  dvdscmulr  16304  divalglem8  16419  ghmgrp  19049  dvfsumlem3  25987  dvfsumrlim  25990  dvfsumrlim2  25991  dvfsumrlim3  25992  dchrisumlem3  27454  dchrisum  27455  abvcxp  27578  padicabv  27593  hvmulcan  31053  isarchi2  33183  archiabllem2c  33193  hasheuni  34116  carsgclctunlem1  34349  carsggect  34350  carsgclctunlem2  34351  carsgclctunlem3  34352  carsgclctun  34353  carsgsiga  34354  omsmeas  34355  pibt2  37435  tendoicl  40815  cdlemkfid2N  40942  erngdvlem4  41010  f1o2d2  42284  pellex  42858  refsumcn  45054  restuni3  45142  wessf1ornlem  45209  unirnmapsn  45238  ssmapsn  45240  iunmapsn  45241  ssfiunibd  45338  supxrgelem  45364  infleinf2  45441  fmuldfeq  45612  limsupmnfuzlem  45755  limsupre3uzlem  45764  cosknegpi  45898  icccncfext  45916  stoweidlem31  46060  stoweidlem43  46072  stoweidlem46  46075  stoweidlem52  46081  stoweidlem53  46082  stoweidlem54  46083  stoweidlem55  46084  stoweidlem56  46085  stoweidlem57  46086  stoweidlem58  46087  stoweidlem59  46088  stoweidlem60  46089  stoweidlem62  46091  stoweid  46092  fourierdlem12  46148  fourierdlem41  46177  fourierdlem48  46183  fourierdlem79  46214  fourierdlem81  46216  etransclem24  46287  etransclem46  46309  sge0f1o  46411  sge0iunmptlemre  46444  sge0iunmpt  46447  sge0seq  46475  caragenfiiuncl  46544  hoicvr  46577  hoidmvval0  46616  hspmbllem2  46656  smflimsuplem7  46855  el0ldep  48442  2arymaptfo  48634  itschlc0yqe  48740  itsclc0yqsol  48744