Theorem 3adant1r 1178

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 1163	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  8796  isf32lem9  10321  axdc3lem4  10413  tskun  10746  dvdscmulr  16261  divalglem8  16377  ghmgrp  19005  dvfsumlem3  25942  dvfsumrlim  25945  dvfsumrlim2  25946  dvfsumrlim3  25947  dchrisumlem3  27409  dchrisum  27410  abvcxp  27533  padicabv  27548  hvmulcan  31008  isarchi2  33146  archiabllem2c  33156  hasheuni  34082  carsgclctunlem1  34315  carsggect  34316  carsgclctunlem2  34317  carsgclctunlem3  34318  carsgclctun  34319  carsgsiga  34320  omsmeas  34321  pibt2  37412  tendoicl  40797  cdlemkfid2N  40924  erngdvlem4  40992  f1o2d2  42228  pellex  42830  refsumcn  45031  restuni3  45119  wessf1ornlem  45186  unirnmapsn  45215  ssmapsn  45217  iunmapsn  45218  ssfiunibd  45314  supxrgelem  45340  infleinf2  45417  fmuldfeq  45588  limsupmnfuzlem  45731  limsupre3uzlem  45740  cosknegpi  45874  icccncfext  45892  stoweidlem31  46036  stoweidlem43  46048  stoweidlem46  46051  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  stoweidlem55  46060  stoweidlem56  46061  stoweidlem57  46062  stoweidlem58  46063  stoweidlem59  46064  stoweidlem60  46065  stoweidlem62  46067  stoweid  46068  fourierdlem12  46124  fourierdlem41  46153  fourierdlem48  46159  fourierdlem79  46190  fourierdlem81  46192  etransclem24  46263  etransclem46  46285  sge0f1o  46387  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0seq  46451  caragenfiiuncl  46520  hoicvr  46553  hoidmvval0  46592  hspmbllem2  46632  smflimsuplem7  46831  el0ldep  48459  2arymaptfo  48647  itschlc0yqe  48753  itsclc0yqsol  48757