Theorem 3adant1r 1196

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mpof1o2d  8137  ecopovtrn  8841  rankfilimbi  9902  isf32lem9  10439  axdc3lem4  10531  tskun  10871  dvdscmulr  16454  divalglem8  16570  ghmgrp  19276  dvfsumlem3  26348  dvfsumrlim  26351  dvfsumrlim2  26352  dvfsumrlim3  26353  dchrisumlem3  27818  dchrisum  27819  abvcxp  27942  padicabv  27957  hvmulcan  31674  isarchi2  33746  archiabllem2c  33756  hasheuni  34717  carsgclctunlem1  34949  carsggect  34950  carsgclctunlem2  34951  carsgclctunlem3  34952  carsgclctun  34953  carsgsiga  34954  omsmeas  34955  pibt2  38340  tendoicl  41853  cdlemkfid2N  41980  erngdvlem4  42048  pellex  43841  refsumcn  46046  restuni3  46132  wessf1ornlem  46199  unirnmapsn  46226  ssmapsn  46228  iunmapsn  46229  ssfiunibd  46324  supxrgelem  46348  infleinf2  46423  fmuldfeq  46594  limsupmnfuzlem  46735  limsupre3uzlem  46744  cosknegpi  46878  icccncfext  46896  stoweidlem31  47040  stoweidlem43  47052  stoweidlem46  47055  stoweidlem52  47061  stoweidlem53  47062  stoweidlem54  47063  stoweidlem55  47064  stoweidlem56  47065  stoweidlem57  47066  stoweidlem58  47067  stoweidlem59  47068  stoweidlem60  47069  stoweidlem62  47071  stoweid  47072  fourierdlem12  47128  fourierdlem41  47157  fourierdlem48  47163  fourierdlem79  47194  fourierdlem81  47196  etransclem24  47267  etransclem46  47289  sge0f1o  47391  sge0iunmptlemre  47424  sge0iunmpt  47427  sge0seq  47455  caragenfiiuncl  47524  hoicvr  47557  hoidmvval0  47596  hspmbllem2  47636  smflimsuplem7  47835  el0ldep  49577  2arymaptfo  49765  itschlc0yqe  49871  itsclc0yqsol  49875