Theorem simplrd 782

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 500	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 501	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  erinxp  8791  fpwwe2lem5  10644  fpwwe2lem6  10645  fpwwe2lem8  10647  lejoin2  18471  lemeet2  18485  dirdm  18688  dirref  18689  lmhmlmod2  21216  pi1cpbl  25272  pntlemr  27838  hlgrcl2  28946  oppne2  29097  dfcgra2  29217  cgraer  29256  angmgmlem  29274  prlngrcl2  29300  mgcf2  33429  mgccole2  33431  mgcmnt1  33432  mgcmnt2  33433  mgcf1olem1  33441  mgcf1olem2  33442  mgcf1o  33443  erlcl2  33701  erler  33705  mtyf2  36130  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  fourierdlem48  46982  fourierdlem76  47010  fourierdlem80  47014  fourierdlem93  47027  fourierdlem94  47028  fourierdlem104  47038  fourierdlem113  47047  mea0  47282  meaiunlelem  47296  meaiuninclem  47308  omessle  47326  omedm  47327  carageniuncllem2  47350  hspmbllem3  47456  sectpropdlem  49962  invpropdlem  49964  isopropdlem  49966  uprcl5  50118