Theorem 3adant1r 1177

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 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  8878  isf32lem9  10430  axdc3lem4  10522  tskun  10855  dvdscmulr  16333  divalglem8  16448  ghmgrp  19106  dvfsumlem3  26089  dvfsumrlim  26092  dvfsumrlim2  26093  dvfsumrlim3  26094  dchrisumlem3  27553  dchrisum  27554  abvcxp  27677  padicabv  27692  hvmulcan  31104  isarchi2  33165  archiabllem2c  33175  hasheuni  34049  carsgclctunlem1  34282  carsggect  34283  carsgclctunlem2  34284  carsgclctunlem3  34285  carsgclctun  34286  carsgsiga  34287  omsmeas  34288  pibt2  37383  tendoicl  40753  cdlemkfid2N  40880  erngdvlem4  40948  f1o2d2  42228  pellex  42791  refsumcn  44930  restuni3  45020  wessf1ornlem  45092  unirnmapsn  45121  ssmapsn  45123  iunmapsn  45124  ssfiunibd  45224  supxrgelem  45252  infleinf2  45329  fmuldfeq  45504  limsupmnfuzlem  45647  limsupre3uzlem  45656  cosknegpi  45790  icccncfext  45808  stoweidlem31  45952  stoweidlem43  45964  stoweidlem46  45967  stoweidlem52  45973  stoweidlem53  45974  stoweidlem54  45975  stoweidlem55  45976  stoweidlem56  45977  stoweidlem57  45978  stoweidlem58  45979  stoweidlem59  45980  stoweidlem60  45981  stoweidlem62  45983  stoweid  45984  fourierdlem12  46040  fourierdlem41  46069  fourierdlem48  46075  fourierdlem79  46106  fourierdlem81  46108  etransclem24  46179  etransclem46  46201  sge0f1o  46303  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0seq  46367  caragenfiiuncl  46436  hoicvr  46469  hoidmvval0  46508  hspmbllem2  46548  smflimsuplem7  46747  el0ldep  48195  2arymaptfo  48388  itschlc0yqe  48494  itsclc0yqsol  48498