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  8728  fpwwe2lem5  10546  fpwwe2lem6  10547  fpwwe2lem8  10549  lejoin2  18306  lemeet2  18320  dirdm  18523  dirref  18524  lmhmlmod2  20984  pi1cpbl  25000  pntlemr  27569  oppne2  28814  dfcgra2  28902  mgcf2  33071  mgccole2  33073  mgcmnt1  33074  mgcmnt2  33075  mgcf1olem1  33083  mgcf1olem2  33084  mgcf1o  33085  erlcl2  33343  erler  33347  mtyf2  35745  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  fourierdlem48  46398  fourierdlem76  46426  fourierdlem80  46430  fourierdlem93  46443  fourierdlem94  46444  fourierdlem104  46454  fourierdlem113  46463  mea0  46698  meaiunlelem  46712  meaiuninclem  46724  omessle  46742  omedm  46743  carageniuncllem2  46766  hspmbllem3  46872  sectpropdlem  49281  invpropdlem  49283  isopropdlem  49285  uprcl5  49437