Theorem 3adant1r 1176

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ecopovtrn  8609  isf32lem9  10117  axdc3lem4  10209  tskun  10542  dvdscmulr  15994  divalglem8  16109  ghmgrp  18699  dvfsumlem3  25192  dvfsumrlim  25195  dvfsumrlim2  25196  dvfsumrlim3  25197  dchrisumlem3  26639  dchrisum  26640  abvcxp  26763  padicabv  26778  hvmulcan  29434  isarchi2  31439  archiabllem2c  31449  hasheuni  32053  carsgclctunlem1  32284  carsggect  32285  carsgclctunlem2  32286  carsgclctunlem3  32287  carsgclctun  32288  carsgsiga  32289  omsmeas  32290  pibt2  35588  tendoicl  38810  cdlemkfid2N  38937  erngdvlem4  39005  pellex  40657  refsumcn  42573  restuni3  42667  wessf1ornlem  42722  unirnmapsn  42754  ssmapsn  42756  iunmapsn  42757  ssfiunibd  42848  supxrgelem  42876  infleinf2  42954  fmuldfeq  43124  limsupmnfuzlem  43267  limsupre3uzlem  43276  cosknegpi  43410  icccncfext  43428  stoweidlem31  43572  stoweidlem43  43584  stoweidlem46  43587  stoweidlem52  43593  stoweidlem53  43594  stoweidlem54  43595  stoweidlem55  43596  stoweidlem56  43597  stoweidlem57  43598  stoweidlem58  43599  stoweidlem59  43600  stoweidlem60  43601  stoweidlem62  43603  stoweid  43604  fourierdlem12  43660  fourierdlem41  43689  fourierdlem48  43695  fourierdlem79  43726  fourierdlem81  43728  etransclem24  43799  etransclem46  43821  sge0f1o  43920  sge0iunmptlemre  43953  sge0iunmpt  43956  sge0seq  43984  caragenfiiuncl  44053  hoicvr  44086  hoidmvval0  44125  hspmbllem2  44165  smflimsuplem7  44359  el0ldep  45807  2arymaptfo  46000  itschlc0yqe  46106  itsclc0yqsol  46110