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  8140  ecopovtrn  8845  rankfilimbi  9906  isf32lem9  10443  axdc3lem4  10535  tskun  10875  dvdscmulr  16460  divalglem8  16576  ghmgrp  19282  dvfsumlem3  26354  dvfsumrlim  26357  dvfsumrlim2  26358  dvfsumrlim3  26359  dchrisumlem3  27824  dchrisum  27825  abvcxp  27948  padicabv  27963  hvmulcan  31680  isarchi2  33793  archiabllem2c  33803  hasheuni  34764  carsgclctunlem1  34996  carsggect  34997  carsgclctunlem2  34998  carsgclctunlem3  34999  carsgclctun  35000  carsgsiga  35001  omsmeas  35002  pibt2  38434  tendoicl  41947  cdlemkfid2N  42074  erngdvlem4  42142  pellex  43936  refsumcn  46141  restuni3  46227  wessf1ornlem  46294  unirnmapsn  46321  ssmapsn  46323  iunmapsn  46324  ssfiunibd  46419  supxrgelem  46443  infleinf2  46518  fmuldfeq  46689  limsupmnfuzlem  46830  limsupre3uzlem  46839  cosknegpi  46973  icccncfext  46991  stoweidlem31  47135  stoweidlem43  47147  stoweidlem46  47150  stoweidlem52  47156  stoweidlem53  47157  stoweidlem54  47158  stoweidlem55  47159  stoweidlem56  47160  stoweidlem57  47161  stoweidlem58  47162  stoweidlem59  47163  stoweidlem60  47164  stoweidlem62  47166  stoweid  47167  fourierdlem12  47223  fourierdlem41  47252  fourierdlem48  47258  fourierdlem79  47289  fourierdlem81  47291  etransclem24  47362  etransclem46  47384  sge0f1o  47486  sge0iunmptlemre  47519  sge0iunmpt  47522  sge0seq  47550  caragenfiiuncl  47619  hoicvr  47652  hoidmvval0  47691  hspmbllem2  47731  smflimsuplem7  47930  el0ldep  49672  2arymaptfo  49860  itschlc0yqe  49966  itsclc0yqsol  49970