Theorem 3adant1r 1194

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 487	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an1 1179	1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mpof1o2d  8109  ecopovtrn  8806  isf32lem9  10333  axdc3lem4  10425  tskun  10759  dvdscmulr  16330  divalglem8  16446  ghmgrp  19120  dvfsumlem3  26144  dvfsumrlim  26147  dvfsumrlim2  26148  dvfsumrlim3  26149  dchrisumlem3  27609  dchrisum  27610  abvcxp  27733  padicabv  27748  hvmulcan  31329  isarchi2  33413  archiabllem2c  33423  hasheuni  34387  carsgclctunlem1  34619  carsggect  34620  carsgclctunlem2  34621  carsgclctunlem3  34622  carsgclctun  34623  carsgsiga  34624  omsmeas  34625  rankfilimbi  35404  pibt2  37918  tendoicl  41427  cdlemkfid2N  41554  erngdvlem4  41622  pellex  43419  refsumcn  45609  restuni3  45695  wessf1ornlem  45762  unirnmapsn  45789  ssmapsn  45791  iunmapsn  45792  ssfiunibd  45887  supxrgelem  45912  infleinf2  45987  fmuldfeq  46158  limsupmnfuzlem  46299  limsupre3uzlem  46308  cosknegpi  46442  icccncfext  46460  stoweidlem31  46604  stoweidlem43  46616  stoweidlem46  46619  stoweidlem52  46625  stoweidlem53  46626  stoweidlem54  46627  stoweidlem55  46628  stoweidlem56  46629  stoweidlem57  46630  stoweidlem58  46631  stoweidlem59  46632  stoweidlem60  46633  stoweidlem62  46635  stoweid  46636  fourierdlem12  46692  fourierdlem41  46721  fourierdlem48  46727  fourierdlem79  46758  fourierdlem81  46760  etransclem24  46831  etransclem46  46853  sge0f1o  46955  sge0iunmptlemre  46988  sge0iunmpt  46991  sge0seq  47019  caragenfiiuncl  47088  hoicvr  47121  hoidmvval0  47160  hspmbllem2  47200  smflimsuplem7  47399  el0ldep  49098  2arymaptfo  49286  itschlc0yqe  49392  itsclc0yqsol  49396