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 ⊢ (𝜑 → 𝜒)

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

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 401

This theorem is used by:  erinxp  8787  fpwwe2lem5  10626  fpwwe2lem6  10627  fpwwe2lem8  10629  lejoin2  18445  lemeet2  18459  dirdm  18662  dirref  18663  lmhmlmod2  21164  pi1cpbl  25214  pntlemr  27777  hlgrcl2  28884  oppne2  29034  dfcgra2  29152  prlngrcl2  29204  mgcf2  33318  mgccole2  33320  mgcmnt1  33321  mgcmnt2  33322  mgcf1olem1  33330  mgcf1olem2  33331  mgcf1o  33332  erlcl2  33590  erler  33594  mtyf2  36051  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  fourierdlem48  46896  fourierdlem76  46924  fourierdlem80  46928  fourierdlem93  46941  fourierdlem94  46942  fourierdlem104  46952  fourierdlem113  46961  mea0  47196  meaiunlelem  47210  meaiuninclem  47222  omessle  47240  omedm  47241  carageniuncllem2  47264  hspmbllem3  47370  sectpropdlem  49842  invpropdlem  49844  isopropdlem  49846  uprcl5  49998