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  8630  fpwwe2lem5  10471  fpwwe2lem6  10472  fpwwe2lem8  10474  lejoin2  18180  lemeet2  18194  dirdm  18395  dirref  18396  lmhmlmod2  20377  pi1cpbl  24290  pntlemr  26833  oppne2  27239  dfcgra2  27327  mgcf2  31402  mgccole2  31404  mgcmnt1  31405  mgcmnt2  31406  mgcf1olem1  31414  mgcf1olem2  31415  mgcf1o  31416  mtyf2  33652  ioodvbdlimc1lem2  43723  ioodvbdlimc2lem  43725  fourierdlem48  43945  fourierdlem76  43973  fourierdlem80  43977  fourierdlem93  43990  fourierdlem94  43991  fourierdlem104  44001  fourierdlem113  44010  mea0  44243  meaiunlelem  44257  meaiuninclem  44269  omessle  44287  omedm  44288  carageniuncllem2  44311  hspmbllem3  44417