Theorem simplrd 767

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  erinxp  8580  fpwwe2lem5  10391  fpwwe2lem6  10392  fpwwe2lem8  10394  lejoin2  18103  lemeet2  18117  dirdm  18318  dirref  18319  lmhmlmod2  20294  pi1cpbl  24207  pntlemr  26750  oppne2  27103  dfcgra2  27191  mgcf2  31267  mgccole2  31269  mgcmnt1  31270  mgcmnt2  31271  mgcf1olem1  31279  mgcf1olem2  31280  mgcf1o  31281  mtyf2  33513  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  fourierdlem48  43695  fourierdlem76  43723  fourierdlem80  43727  fourierdlem93  43740  fourierdlem94  43741  fourierdlem104  43751  fourierdlem113  43760  mea0  43992  meaiunlelem  44006  meaiuninclem  44018  omessle  44036  omedm  44037  carageniuncllem2  44060  hspmbllem3  44166