Theorem 3adant1r 1176

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

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

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 1088

This theorem is referenced by:  ecopovtrn  8858  isf32lem9  10398  axdc3lem4  10490  tskun  10823  dvdscmulr  16318  divalglem8  16433  ghmgrp  19096  dvfsumlem3  26083  dvfsumrlim  26086  dvfsumrlim2  26087  dvfsumrlim3  26088  dchrisumlem3  27549  dchrisum  27550  abvcxp  27673  padicabv  27688  hvmulcan  31100  isarchi2  33174  archiabllem2c  33184  hasheuni  34065  carsgclctunlem1  34298  carsggect  34299  carsgclctunlem2  34300  carsgclctunlem3  34301  carsgclctun  34302  carsgsiga  34303  omsmeas  34304  pibt2  37399  tendoicl  40778  cdlemkfid2N  40905  erngdvlem4  40973  f1o2d2  42252  pellex  42822  refsumcn  44967  restuni3  45057  wessf1ornlem  45127  unirnmapsn  45156  ssmapsn  45158  iunmapsn  45159  ssfiunibd  45259  supxrgelem  45286  infleinf2  45363  fmuldfeq  45538  limsupmnfuzlem  45681  limsupre3uzlem  45690  cosknegpi  45824  icccncfext  45842  stoweidlem31  45986  stoweidlem43  45998  stoweidlem46  46001  stoweidlem52  46007  stoweidlem53  46008  stoweidlem54  46009  stoweidlem55  46010  stoweidlem56  46011  stoweidlem57  46012  stoweidlem58  46013  stoweidlem59  46014  stoweidlem60  46015  stoweidlem62  46017  stoweid  46018  fourierdlem12  46074  fourierdlem41  46103  fourierdlem48  46109  fourierdlem79  46140  fourierdlem81  46142  etransclem24  46213  etransclem46  46235  sge0f1o  46337  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0seq  46401  caragenfiiuncl  46470  hoicvr  46503  hoidmvval0  46542  hspmbllem2  46582  smflimsuplem7  46781  el0ldep  48311  2arymaptfo  48503  itschlc0yqe  48609  itsclc0yqsol  48613