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  8373  fpwwe2lem6  10059  fpwwe2lem7  10060  fpwwe2lem9  10062  lejoin2  17625  lemeet2  17639  dirdm  17846  dirref  17847  lmhmlmod2  19806  pi1cpbl  23650  pntlemr  26180  oppne2  26530  dfcgra2  26618  mtyf2  32800  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  fourierdlem48  42446  fourierdlem76  42474  fourierdlem80  42478  fourierdlem93  42491  fourierdlem94  42492  fourierdlem104  42502  fourierdlem113  42511  mea0  42743  meaiunlelem  42757  meaiuninclem  42769  omessle  42787  omedm  42788  carageniuncllem2  42811  hspmbllem3  42917