Theorem simplrd 779

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  erinxp  8766  fpwwe2lem5  10586  fpwwe2lem6  10587  fpwwe2lem8  10589  lejoin2  18405  lemeet2  18419  dirdm  18622  dirref  18623  lmhmlmod2  21086  pi1cpbl  25093  pntlemr  27653  oppne2  28898  dfcgra2  28986  mgcf2  33127  mgccole2  33129  mgcmnt1  33130  mgcmnt2  33131  mgcf1olem1  33139  mgcf1olem2  33140  mgcf1o  33141  erlcl2  33402  erler  33406  mtyf2  35861  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  fourierdlem48  46688  fourierdlem76  46716  fourierdlem80  46720  fourierdlem93  46733  fourierdlem94  46734  fourierdlem104  46744  fourierdlem113  46753  mea0  46988  meaiunlelem  47002  meaiuninclem  47014  omessle  47032  omedm  47033  carageniuncllem2  47056  hspmbllem3  47162  sectpropdlem  49617  invpropdlem  49619  isopropdlem  49621  uprcl5  49773