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  8850  fpwwe2lem5  10759  fpwwe2lem6  10760  fpwwe2lem8  10762  lejoin2  18607  lemeet2  18621  dirdm  18824  dirref  18825  lmhmlmod2  21358  pi1cpbl  25420  pntlemr  27986  hlgrcl2  29124  oppne2  29275  dfcgra2  29395  cgraer  29434  angmgmlem  29452  prlngrcl2  29478  mgcf2  33649  mgccole2  33651  mgcmnt1  33652  mgcmnt2  33653  mgcf1olem1  33661  mgcf1olem2  33662  mgcf1o  33663  erlcl2  33921  erler  33925  mtyf2  36524  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  fourierdlem48  47437  fourierdlem76  47465  fourierdlem80  47469  fourierdlem93  47482  fourierdlem94  47483  fourierdlem104  47493  fourierdlem113  47502  mea0  47737  meaiunlelem  47751  meaiuninclem  47763  omessle  47781  omedm  47782  carageniuncllem2  47805  hspmbllem3  47911  sectpropdlem  50481  invpropdlem  50483  isopropdlem  50485  uprcl5  50639