Theorem 3adant1r 1175

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 1161	1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ecopovtrn  8567  isf32lem9  10048  axdc3lem4  10140  tskun  10473  dvdscmulr  15922  divalglem8  16037  ghmgrp  18614  dvfsumlem3  25097  dvfsumrlim  25100  dvfsumrlim2  25101  dvfsumrlim3  25102  dchrisumlem3  26544  dchrisum  26545  abvcxp  26668  padicabv  26683  hvmulcan  29335  isarchi2  31341  archiabllem2c  31351  hasheuni  31953  carsgclctunlem1  32184  carsggect  32185  carsgclctunlem2  32186  carsgclctunlem3  32187  carsgclctun  32188  carsgsiga  32189  omsmeas  32190  pibt2  35515  tendoicl  38737  cdlemkfid2N  38864  erngdvlem4  38932  pellex  40573  refsumcn  42462  restuni3  42556  wessf1ornlem  42611  unirnmapsn  42643  ssmapsn  42645  iunmapsn  42646  ssfiunibd  42738  supxrgelem  42766  infleinf2  42844  fmuldfeq  43014  limsupmnfuzlem  43157  limsupre3uzlem  43166  cosknegpi  43300  icccncfext  43318  stoweidlem31  43462  stoweidlem43  43474  stoweidlem46  43477  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  stoweidlem55  43486  stoweidlem56  43487  stoweidlem57  43488  stoweidlem58  43489  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  stoweid  43494  fourierdlem12  43550  fourierdlem41  43579  fourierdlem48  43585  fourierdlem79  43616  fourierdlem81  43618  etransclem24  43689  etransclem46  43711  sge0f1o  43810  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0seq  43874  caragenfiiuncl  43943  hoicvr  43976  hoidmvval0  44015  hspmbllem2  44055  smflimsuplem7  44246  el0ldep  45695  2arymaptfo  45888  itschlc0yqe  45994  itsclc0yqsol  45998