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  8725  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  lejoin2  18307  lemeet2  18321  dirdm  18524  dirref  18525  lmhmlmod2  20954  pi1cpbl  24960  pntlemr  27529  oppne2  28705  dfcgra2  28793  mgcf2  32944  mgccole2  32946  mgcmnt1  32947  mgcmnt2  32948  mgcf1olem1  32956  mgcf1olem2  32957  mgcf1o  32958  erlcl2  33214  erler  33218  mtyf2  35526  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  fourierdlem48  46139  fourierdlem76  46167  fourierdlem80  46171  fourierdlem93  46184  fourierdlem94  46185  fourierdlem104  46195  fourierdlem113  46204  mea0  46439  meaiunlelem  46453  meaiuninclem  46465  omessle  46483  omedm  46484  carageniuncllem2  46507  hspmbllem3  46613  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029  uprcl5  49181