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  8764  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  lejoin2  18344  lemeet2  18358  dirdm  18559  dirref  18560  lmhmlmod2  20939  pi1cpbl  24944  pntlemr  27513  oppne2  28669  dfcgra2  28757  mgcf2  32915  mgccole2  32917  mgcmnt1  32918  mgcmnt2  32919  mgcf1olem1  32927  mgcf1olem2  32928  mgcf1o  32929  erlcl2  33212  erler  33216  mtyf2  35538  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  fourierdlem48  46152  fourierdlem76  46180  fourierdlem80  46184  fourierdlem93  46197  fourierdlem94  46198  fourierdlem104  46208  fourierdlem113  46217  mea0  46452  meaiunlelem  46466  meaiuninclem  46478  omessle  46496  omedm  46497  carageniuncllem2  46520  hspmbllem3  46626  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029  uprcl5  49181