Theorem simplrd 789

Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

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

Assertion

Ref	Expression
simplrd	⊢ (𝜑 → 𝜒)

Proof of Theorem simplrd

Step	Hyp	Ref	Expression
1		simplrd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
2	1	simpld 474	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 478	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383

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

This theorem is referenced by:  dfcgra2  25521  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  fourierdlem48  39047  fourierdlem76  39075  fourierdlem80  39079  fourierdlem93  39092  fourierdlem94  39093  fourierdlem104  39103  fourierdlem113  39112  ismea  39344  mea0  39347  meaiunlelem  39361  meaiuninclem  39373  omessle  39388  omedm  39389  carageniuncllem2  39412  hspmbllem3  39518  isclwwlksng  41196