Theorem 3adant1r 1311

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
3adant1l.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant1r	⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant1r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1258	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	adantlr 747	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	3	3impb 1252	1 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3adant2r  1313  3adant3r  1315  ecopovtrn  7737  isf32lem9  9066  axdc3lem4  9158  tskun  9487  dvdscmulr  14848  divalglem8  14961  ghmgrp  17362  quscrng  19061  dvfsumlem3  23595  dvfsumrlim  23598  dvfsumrlim2  23599  dvfsumrlim3  23600  dchrisumlem3  24980  dchrisum  24981  abvcxp  25104  padicabv  25119  hvmulcan  27313  isarchi2  29070  archiabllem2c  29080  hasheuni  29474  carsgclctunlem1  29706  carsggect  29707  carsgclctunlem2  29708  carsgclctunlem3  29709  carsgclctun  29710  carsgsiga  29711  omsmeas  29712  tendoicl  35102  cdlemkfid2N  35229  erngdvlem4  35297  pellex  36417  refsumcn  38212  restuni3  38333  wessf1ornlem  38366  unirnmapsn  38401  ssmapsn  38403  iunmapsn  38404  ssfiunibd  38464  supxrgelem  38494  fmuldfeq  38650  cosknegpi  38752  icccncfext  38773  stoweidlem31  38924  stoweidlem43  38936  stoweidlem46  38939  stoweidlem52  38945  stoweidlem53  38946  stoweidlem54  38947  stoweidlem55  38948  stoweidlem56  38949  stoweidlem57  38950  stoweidlem58  38951  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  stoweid  38956  fourierdlem12  39012  fourierdlem41  39041  fourierdlem48  39047  fourierdlem79  39078  fourierdlem81  39080  etransclem24  39151  etransclem46  39173  sge0f1o  39275  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0seq  39339  caragenfiiuncl  39405  hoicvr  39438  hoidmvval0  39477  hspmbllem2  39517  el0ldep  42049