Theorem simplrd 766

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

This theorem is referenced by:  erinxp  8538  fpwwe2lem5  10322  fpwwe2lem6  10323  fpwwe2lem8  10325  lejoin2  18018  lemeet2  18032  dirdm  18233  dirref  18234  lmhmlmod2  20209  pi1cpbl  24113  pntlemr  26655  oppne2  27007  dfcgra2  27095  mgcf2  31169  mgccole2  31171  mgcmnt1  31172  mgcmnt2  31173  mgcf1olem1  31181  mgcf1olem2  31182  mgcf1o  31183  mtyf2  33413  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  fourierdlem48  43585  fourierdlem76  43613  fourierdlem80  43617  fourierdlem93  43630  fourierdlem94  43631  fourierdlem104  43641  fourierdlem113  43650  mea0  43882  meaiunlelem  43896  meaiuninclem  43908  omessle  43926  omedm  43927  carageniuncllem2  43950  hspmbllem3  44056