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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  erinxp  8785  fpwwe2lem5  10630  fpwwe2lem6  10631  fpwwe2lem8  10633  lejoin2  18338  lemeet2  18352  dirdm  18553  dirref  18554  lmhmlmod2  20643  pi1cpbl  24560  pntlemr  27105  oppne2  28024  dfcgra2  28112  mgcf2  32190  mgccole2  32192  mgcmnt1  32193  mgcmnt2  32194  mgcf1olem1  32202  mgcf1olem2  32203  mgcf1o  32204  mtyf2  34573  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  fourierdlem48  44918  fourierdlem76  44946  fourierdlem80  44950  fourierdlem93  44963  fourierdlem94  44964  fourierdlem104  44974  fourierdlem113  44983  mea0  45218  meaiunlelem  45232  meaiuninclem  45244  omessle  45262  omedm  45263  carageniuncllem2  45286  hspmbllem3  45392