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  8769  isf32lem9  10283  axdc3lem4  10375  tskun  10709  dvdscmulr  16223  divalglem8  16339  ghmgrp  19008  dvfsumlem3  26003  dvfsumrlim  26006  dvfsumrlim2  26007  dvfsumrlim3  26008  dchrisumlem3  27470  dchrisum  27471  abvcxp  27594  padicabv  27609  hvmulcan  31159  isarchi2  33278  archiabllem2c  33288  hasheuni  34262  carsgclctunlem1  34494  carsggect  34495  carsgclctunlem2  34496  carsgclctunlem3  34497  carsgclctun  34498  carsgsiga  34499  omsmeas  34500  rankfilimbi  35276  pibt2  37669  tendoicl  41169  cdlemkfid2N  41296  erngdvlem4  41364  f1o2d2  42602  pellex  43189  refsumcn  45387  restuni3  45474  wessf1ornlem  45541  unirnmapsn  45569  ssmapsn  45571  iunmapsn  45572  ssfiunibd  45668  supxrgelem  45693  infleinf2  45769  fmuldfeq  45940  limsupmnfuzlem  46081  limsupre3uzlem  46090  cosknegpi  46224  icccncfext  46242  stoweidlem31  46386  stoweidlem43  46398  stoweidlem46  46401  stoweidlem52  46407  stoweidlem53  46408  stoweidlem54  46409  stoweidlem55  46410  stoweidlem56  46411  stoweidlem57  46412  stoweidlem58  46413  stoweidlem59  46414  stoweidlem60  46415  stoweidlem62  46417  stoweid  46418  fourierdlem12  46474  fourierdlem41  46503  fourierdlem48  46509  fourierdlem79  46540  fourierdlem81  46542  etransclem24  46613  etransclem46  46635  sge0f1o  46737  sge0iunmptlemre  46770  sge0iunmpt  46773  sge0seq  46801  caragenfiiuncl  46870  hoicvr  46903  hoidmvval0  46942  hspmbllem2  46982  smflimsuplem7  47181  el0ldep  48823  2arymaptfo  49011  itschlc0yqe  49117  itsclc0yqsol  49121