Theorem simplrd 768

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 497	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 498	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  erinxp  8371  fpwwe2lem6  10057  fpwwe2lem7  10058  fpwwe2lem9  10060  lejoin2  17623  lemeet2  17637  dirdm  17844  dirref  17845  lmhmlmod2  19804  pi1cpbl  23648  pntlemr  26178  oppne2  26528  dfcgra2  26616  mtyf2  32798  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  fourierdlem48  42459  fourierdlem76  42487  fourierdlem80  42491  fourierdlem93  42504  fourierdlem94  42505  fourierdlem104  42515  fourierdlem113  42524  mea0  42756  meaiunlelem  42770  meaiuninclem  42782  omessle  42800  omedm  42801  carageniuncllem2  42824  hspmbllem3  42930