Theorem simplrd 770

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  erinxp  8740  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  lejoin2  18318  lemeet2  18332  dirdm  18535  dirref  18536  lmhmlmod2  20996  pi1cpbl  25012  pntlemr  27581  oppne2  28826  dfcgra2  28914  mgcf2  33081  mgccole2  33083  mgcmnt1  33084  mgcmnt2  33085  mgcf1olem1  33093  mgcf1olem2  33094  mgcf1o  33095  erlcl2  33354  erler  33358  mtyf2  35764  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  fourierdlem48  46509  fourierdlem76  46537  fourierdlem80  46541  fourierdlem93  46554  fourierdlem94  46555  fourierdlem104  46565  fourierdlem113  46574  mea0  46809  meaiunlelem  46823  meaiuninclem  46835  omessle  46853  omedm  46854  carageniuncllem2  46877  hspmbllem3  46983  sectpropdlem  49392  invpropdlem  49394  isopropdlem  49396  uprcl5  49548