Theorem simplrd 769

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  8849  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  lejoin2  18455  lemeet2  18469  dirdm  18670  dirref  18671  lmhmlmod2  21054  pi1cpbl  25096  pntlemr  27664  oppne2  28768  dfcgra2  28856  mgcf2  32962  mgccole2  32964  mgcmnt1  32965  mgcmnt2  32966  mgcf1olem1  32974  mgcf1olem2  32975  mgcf1o  32976  erlcl2  33233  erler  33237  mtyf2  35519  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  fourierdlem48  46075  fourierdlem76  46103  fourierdlem80  46107  fourierdlem93  46120  fourierdlem94  46121  fourierdlem104  46131  fourierdlem113  46140  mea0  46375  meaiunlelem  46389  meaiuninclem  46401  omessle  46419  omedm  46420  carageniuncllem2  46443  hspmbllem3  46549