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  8744  isf32lem9  10252  axdc3lem4  10344  tskun  10677  dvdscmulr  16195  divalglem8  16311  ghmgrp  18979  dvfsumlem3  25963  dvfsumrlim  25966  dvfsumrlim2  25967  dvfsumrlim3  25968  dchrisumlem3  27430  dchrisum  27431  abvcxp  27554  padicabv  27569  hvmulcan  31050  isarchi2  33152  archiabllem2c  33162  hasheuni  34096  carsgclctunlem1  34328  carsggect  34329  carsgclctunlem2  34330  carsgclctunlem3  34331  carsgclctun  34332  carsgsiga  34333  omsmeas  34334  rankfilimbi  35110  pibt2  37457  tendoicl  40841  cdlemkfid2N  40968  erngdvlem4  41036  f1o2d2  42272  pellex  42874  refsumcn  45073  restuni3  45161  wessf1ornlem  45228  unirnmapsn  45257  ssmapsn  45259  iunmapsn  45260  ssfiunibd  45356  supxrgelem  45382  infleinf2  45458  fmuldfeq  45629  limsupmnfuzlem  45770  limsupre3uzlem  45779  cosknegpi  45913  icccncfext  45931  stoweidlem31  46075  stoweidlem43  46087  stoweidlem46  46090  stoweidlem52  46096  stoweidlem53  46097  stoweidlem54  46098  stoweidlem55  46099  stoweidlem56  46100  stoweidlem57  46101  stoweidlem58  46102  stoweidlem59  46103  stoweidlem60  46104  stoweidlem62  46106  stoweid  46107  fourierdlem12  46163  fourierdlem41  46192  fourierdlem48  46198  fourierdlem79  46229  fourierdlem81  46231  etransclem24  46302  etransclem46  46324  sge0f1o  46426  sge0iunmptlemre  46459  sge0iunmpt  46462  sge0seq  46490  caragenfiiuncl  46559  hoicvr  46592  hoidmvval0  46631  hspmbllem2  46671  smflimsuplem7  46870  el0ldep  48504  2arymaptfo  48692  itschlc0yqe  48798  itsclc0yqsol  48802