Theorem 3adant1r 1177

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  ecopovtrn  8816  isf32lem9  10358  axdc3lem4  10450  tskun  10783  dvdscmulr  16230  divalglem8  16345  ghmgrp  18951  dvfsumlem3  25552  dvfsumrlim  25555  dvfsumrlim2  25556  dvfsumrlim3  25557  dchrisumlem3  27001  dchrisum  27002  abvcxp  27125  padicabv  27140  hvmulcan  30363  isarchi2  32372  archiabllem2c  32382  hasheuni  33152  carsgclctunlem1  33385  carsggect  33386  carsgclctunlem2  33387  carsgclctunlem3  33388  carsgclctun  33389  carsgsiga  33390  omsmeas  33391  pibt2  36384  tendoicl  39753  cdlemkfid2N  39880  erngdvlem4  39948  f1o2d2  41141  pellex  41655  refsumcn  43796  restuni3  43889  wessf1ornlem  43963  unirnmapsn  43992  ssmapsn  43994  iunmapsn  43995  ssfiunibd  44098  supxrgelem  44126  infleinf2  44203  fmuldfeq  44378  limsupmnfuzlem  44521  limsupre3uzlem  44530  cosknegpi  44664  icccncfext  44682  stoweidlem31  44826  stoweidlem43  44838  stoweidlem46  44841  stoweidlem52  44847  stoweidlem53  44848  stoweidlem54  44849  stoweidlem55  44850  stoweidlem56  44851  stoweidlem57  44852  stoweidlem58  44853  stoweidlem59  44854  stoweidlem60  44855  stoweidlem62  44857  stoweid  44858  fourierdlem12  44914  fourierdlem41  44943  fourierdlem48  44949  fourierdlem79  44980  fourierdlem81  44982  etransclem24  45053  etransclem46  45075  sge0f1o  45177  sge0iunmptlemre  45210  sge0iunmpt  45213  sge0seq  45241  caragenfiiuncl  45310  hoicvr  45343  hoidmvval0  45382  hspmbllem2  45422  smflimsuplem7  45621  el0ldep  47225  2arymaptfo  47418  itschlc0yqe  47524  itsclc0yqsol  47528