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  8757  isf32lem9  10271  axdc3lem4  10363  tskun  10697  dvdscmulr  16211  divalglem8  16327  ghmgrp  18996  dvfsumlem3  25991  dvfsumrlim  25994  dvfsumrlim2  25995  dvfsumrlim3  25996  dchrisumlem3  27458  dchrisum  27459  abvcxp  27582  padicabv  27597  hvmulcan  31147  isarchi2  33267  archiabllem2c  33277  hasheuni  34242  carsgclctunlem1  34474  carsggect  34475  carsgclctunlem2  34476  carsgclctunlem3  34477  carsgclctun  34478  carsgsiga  34479  omsmeas  34480  rankfilimbi  35257  pibt2  37622  tendoicl  41056  cdlemkfid2N  41183  erngdvlem4  41251  f1o2d2  42489  pellex  43077  refsumcn  45275  restuni3  45362  wessf1ornlem  45429  unirnmapsn  45458  ssmapsn  45460  iunmapsn  45461  ssfiunibd  45557  supxrgelem  45582  infleinf2  45658  fmuldfeq  45829  limsupmnfuzlem  45970  limsupre3uzlem  45979  cosknegpi  46113  icccncfext  46131  stoweidlem31  46275  stoweidlem43  46287  stoweidlem46  46290  stoweidlem52  46296  stoweidlem53  46297  stoweidlem54  46298  stoweidlem55  46299  stoweidlem56  46300  stoweidlem57  46301  stoweidlem58  46302  stoweidlem59  46303  stoweidlem60  46304  stoweidlem62  46306  stoweid  46307  fourierdlem12  46363  fourierdlem41  46392  fourierdlem48  46398  fourierdlem79  46429  fourierdlem81  46431  etransclem24  46502  etransclem46  46524  sge0f1o  46626  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0seq  46690  caragenfiiuncl  46759  hoicvr  46792  hoidmvval0  46831  hspmbllem2  46871  smflimsuplem7  47070  el0ldep  48712  2arymaptfo  48900  itschlc0yqe  49006  itsclc0yqsol  49010