Theorem simplrd 781

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  erinxp  8790  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem8  10624  lejoin2  18440  lemeet2  18454  dirdm  18657  dirref  18658  lmhmlmod2  21134  pi1cpbl  25184  pntlemr  27747  hlgrcl2  28854  oppne2  29004  dfcgra2  29122  prlngrcl2  29174  mgcf2  33290  mgccole2  33292  mgcmnt1  33293  mgcmnt2  33294  mgcf1olem1  33302  mgcf1olem2  33303  mgcf1o  33304  erlcl2  33562  erler  33566  mtyf2  36024  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  fourierdlem48  46851  fourierdlem76  46879  fourierdlem80  46883  fourierdlem93  46896  fourierdlem94  46897  fourierdlem104  46907  fourierdlem113  46916  mea0  47151  meaiunlelem  47165  meaiuninclem  47177  omessle  47195  omedm  47196  carageniuncllem2  47219  hspmbllem3  47325  sectpropdlem  49797  invpropdlem  49799  isopropdlem  49801  uprcl5  49953