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  8738  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  lejoin2  18349  lemeet2  18363  dirdm  18566  dirref  18567  lmhmlmod2  21027  pi1cpbl  25011  pntlemr  27565  oppne2  28810  dfcgra2  28898  mgcf2  33049  mgccole2  33051  mgcmnt1  33052  mgcmnt2  33053  mgcf1olem1  33061  mgcf1olem2  33062  mgcf1o  33063  erlcl2  33322  erler  33326  mtyf2  35733  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  fourierdlem48  46582  fourierdlem76  46610  fourierdlem80  46614  fourierdlem93  46627  fourierdlem94  46628  fourierdlem104  46638  fourierdlem113  46647  mea0  46882  meaiunlelem  46896  meaiuninclem  46908  omessle  46926  omedm  46927  carageniuncllem2  46950  hspmbllem3  47056  sectpropdlem  49511  invpropdlem  49513  isopropdlem  49515  uprcl5  49667