Theorem simplrd 810

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 477	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 482	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 197  df-an 385

This theorem is referenced by:  dfcgra2  25841  mtyf2  31676  ioodvbdlimc1lem2  40567  ioodvbdlimc2lem  40569  fourierdlem48  40791  fourierdlem76  40819  fourierdlem80  40823  fourierdlem93  40836  fourierdlem94  40837  fourierdlem104  40847  fourierdlem113  40856  ismea  41088  mea0  41091  meaiunlelem  41105  meaiuninclem  41117  omessle  41135  omedm  41136  carageniuncllem2  41159  hspmbllem3  41265