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 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  8860  isf32lem9  10401  axdc3lem4  10493  tskun  10826  dvdscmulr  16322  divalglem8  16437  ghmgrp  19084  dvfsumlem3  26069  dvfsumrlim  26072  dvfsumrlim2  26073  dvfsumrlim3  26074  dchrisumlem3  27535  dchrisum  27536  abvcxp  27659  padicabv  27674  hvmulcan  31091  isarchi2  33192  archiabllem2c  33202  hasheuni  34086  carsgclctunlem1  34319  carsggect  34320  carsgclctunlem2  34321  carsgclctunlem3  34322  carsgclctun  34323  carsgsiga  34324  omsmeas  34325  pibt2  37418  tendoicl  40798  cdlemkfid2N  40925  erngdvlem4  40993  f1o2d2  42274  pellex  42846  refsumcn  45035  restuni3  45123  wessf1ornlem  45190  unirnmapsn  45219  ssmapsn  45221  iunmapsn  45222  ssfiunibd  45321  supxrgelem  45348  infleinf2  45425  fmuldfeq  45598  limsupmnfuzlem  45741  limsupre3uzlem  45750  cosknegpi  45884  icccncfext  45902  stoweidlem31  46046  stoweidlem43  46058  stoweidlem46  46061  stoweidlem52  46067  stoweidlem53  46068  stoweidlem54  46069  stoweidlem55  46070  stoweidlem56  46071  stoweidlem57  46072  stoweidlem58  46073  stoweidlem59  46074  stoweidlem60  46075  stoweidlem62  46077  stoweid  46078  fourierdlem12  46134  fourierdlem41  46163  fourierdlem48  46169  fourierdlem79  46200  fourierdlem81  46202  etransclem24  46273  etransclem46  46295  sge0f1o  46397  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0seq  46461  caragenfiiuncl  46530  hoicvr  46563  hoidmvval0  46602  hspmbllem2  46642  smflimsuplem7  46841  el0ldep  48383  2arymaptfo  48575  itschlc0yqe  48681  itsclc0yqsol  48685