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  10631  fpwwe2lem6  10632  fpwwe2lem8  10634  lejoin2  18456  lemeet2  18470  dirdm  18673  dirref  18674  lmhmlmod2  21182  pi1cpbl  25232  pntlemr  27795  hlgrcl2  28902  oppne2  29052  dfcgra2  29170  prlngrcl2  29222  mgcf2  33332  mgccole2  33334  mgcmnt1  33335  mgcmnt2  33336  mgcf1olem1  33344  mgcf1olem2  33345  mgcf1o  33346  erlcl2  33604  erler  33608  mtyf2  36056  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  fourierdlem48  46901  fourierdlem76  46929  fourierdlem80  46933  fourierdlem93  46946  fourierdlem94  46947  fourierdlem104  46957  fourierdlem113  46966  mea0  47201  meaiunlelem  47215  meaiuninclem  47227  omessle  47245  omedm  47246  carageniuncllem2  47269  hspmbllem3  47375  sectpropdlem  49847  invpropdlem  49849  isopropdlem  49851  uprcl5  50003