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  8715  fpwwe2lem5  10526  fpwwe2lem6  10527  fpwwe2lem8  10529  lejoin2  18289  lemeet2  18303  dirdm  18506  dirref  18507  lmhmlmod2  20967  pi1cpbl  24972  pntlemr  27541  oppne2  28721  dfcgra2  28809  mgcf2  32968  mgccole2  32970  mgcmnt1  32971  mgcmnt2  32972  mgcf1olem1  32980  mgcf1olem2  32981  mgcf1o  32982  erlcl2  33226  erler  33230  mtyf2  35593  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  fourierdlem48  46198  fourierdlem76  46226  fourierdlem80  46230  fourierdlem93  46243  fourierdlem94  46244  fourierdlem104  46254  fourierdlem113  46263  mea0  46498  meaiunlelem  46512  meaiuninclem  46524  omessle  46542  omedm  46543  carageniuncllem2  46566  hspmbllem3  46672  sectpropdlem  49074  invpropdlem  49076  isopropdlem  49078  uprcl5  49230