Theorem simplrd 770

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  8831  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  lejoin2  18430  lemeet2  18444  dirdm  18645  dirref  18646  lmhmlmod2  21031  pi1cpbl  25077  pntlemr  27646  oppne2  28750  dfcgra2  28838  mgcf2  32979  mgccole2  32981  mgcmnt1  32982  mgcmnt2  32983  mgcf1olem1  32991  mgcf1olem2  32992  mgcf1o  32993  erlcl2  33265  erler  33269  mtyf2  35556  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  fourierdlem48  46169  fourierdlem76  46197  fourierdlem80  46201  fourierdlem93  46214  fourierdlem94  46215  fourierdlem104  46225  fourierdlem113  46234  mea0  46469  meaiunlelem  46483  meaiuninclem  46495  omessle  46513  omedm  46514  carageniuncllem2  46537  hspmbllem3  46643  uprcl5  48944