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  8754  isf32lem9  10274  axdc3lem4  10366  tskun  10699  dvdscmulr  16213  divalglem8  16329  ghmgrp  18963  dvfsumlem3  25951  dvfsumrlim  25954  dvfsumrlim2  25955  dvfsumrlim3  25956  dchrisumlem3  27418  dchrisum  27419  abvcxp  27542  padicabv  27557  hvmulcan  31034  isarchi2  33140  archiabllem2c  33150  hasheuni  34054  carsgclctunlem1  34287  carsggect  34288  carsgclctunlem2  34289  carsgclctunlem3  34290  carsgclctun  34291  carsgsiga  34292  omsmeas  34293  pibt2  37393  tendoicl  40778  cdlemkfid2N  40905  erngdvlem4  40973  f1o2d2  42209  pellex  42811  refsumcn  45011  restuni3  45099  wessf1ornlem  45166  unirnmapsn  45195  ssmapsn  45197  iunmapsn  45198  ssfiunibd  45294  supxrgelem  45320  infleinf2  45397  fmuldfeq  45568  limsupmnfuzlem  45711  limsupre3uzlem  45720  cosknegpi  45854  icccncfext  45872  stoweidlem31  46016  stoweidlem43  46028  stoweidlem46  46031  stoweidlem52  46037  stoweidlem53  46038  stoweidlem54  46039  stoweidlem55  46040  stoweidlem56  46041  stoweidlem57  46042  stoweidlem58  46043  stoweidlem59  46044  stoweidlem60  46045  stoweidlem62  46047  stoweid  46048  fourierdlem12  46104  fourierdlem41  46133  fourierdlem48  46139  fourierdlem79  46170  fourierdlem81  46172  etransclem24  46243  etransclem46  46265  sge0f1o  46367  sge0iunmptlemre  46400  sge0iunmpt  46403  sge0seq  46431  caragenfiiuncl  46500  hoicvr  46533  hoidmvval0  46572  hspmbllem2  46612  smflimsuplem7  46811  el0ldep  48455  2arymaptfo  48643  itschlc0yqe  48749  itsclc0yqsol  48753