Theorem simplrd 781

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  erinxp  8785  fpwwe2lem5  10616  fpwwe2lem6  10617  fpwwe2lem8  10619  lejoin2  18435  lemeet2  18449  dirdm  18652  dirref  18653  lmhmlmod2  21127  pi1cpbl  25168  pntlemr  27728  oppne2  28978  dfcgra2  29094  prlngrcl2  29144  mgcf2  33246  mgccole2  33248  mgcmnt1  33249  mgcmnt2  33250  mgcf1olem1  33258  mgcf1olem2  33259  mgcf1o  33260  erlcl2  33518  erler  33522  mtyf2  35938  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  fourierdlem48  46753  fourierdlem76  46781  fourierdlem80  46785  fourierdlem93  46798  fourierdlem94  46799  fourierdlem104  46809  fourierdlem113  46818  mea0  47053  meaiunlelem  47067  meaiuninclem  47079  omessle  47097  omedm  47098  carageniuncllem2  47121  hspmbllem3  47227  sectpropdlem  49692  invpropdlem  49694  isopropdlem  49696  uprcl5  49848