Theorem 3adant1r 1179

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  8767  isf32lem9  10283  axdc3lem4  10375  tskun  10709  dvdscmulr  16253  divalglem8  16369  ghmgrp  19042  dvfsumlem3  25995  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsumrlim3  26000  dchrisumlem3  27454  dchrisum  27455  abvcxp  27578  padicabv  27593  hvmulcan  31143  isarchi2  33246  archiabllem2c  33256  hasheuni  34229  carsgclctunlem1  34461  carsggect  34462  carsgclctunlem2  34463  carsgclctunlem3  34464  carsgclctun  34465  carsgsiga  34466  omsmeas  34467  rankfilimbi  35244  pibt2  37733  tendoicl  41242  cdlemkfid2N  41369  erngdvlem4  41437  f1o2d2  42674  pellex  43263  refsumcn  45461  restuni3  45548  wessf1ornlem  45615  unirnmapsn  45643  ssmapsn  45645  iunmapsn  45646  ssfiunibd  45742  supxrgelem  45767  infleinf2  45842  fmuldfeq  46013  limsupmnfuzlem  46154  limsupre3uzlem  46163  cosknegpi  46297  icccncfext  46315  stoweidlem31  46459  stoweidlem43  46471  stoweidlem46  46474  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  stoweidlem55  46483  stoweidlem56  46484  stoweidlem57  46485  stoweidlem58  46486  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  stoweid  46491  fourierdlem12  46547  fourierdlem41  46576  fourierdlem48  46582  fourierdlem79  46613  fourierdlem81  46615  etransclem24  46686  etransclem46  46708  sge0f1o  46810  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0seq  46874  caragenfiiuncl  46943  hoicvr  46976  hoidmvval0  47015  hspmbllem2  47055  smflimsuplem7  47254  el0ldep  48942  2arymaptfo  49130  itschlc0yqe  49236  itsclc0yqsol  49240