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  8805  fpwwe2lem5  10713  fpwwe2lem6  10714  fpwwe2lem8  10716  lejoin2  18550  lemeet2  18564  dirdm  18767  dirref  18768  lmhmlmod2  21300  pi1cpbl  25358  pntlemr  27922  hlgrcl2  29060  oppne2  29211  dfcgra2  29331  cgraer  29370  angmgmlem  29388  prlngrcl2  29414  mgcf2  33543  mgccole2  33545  mgcmnt1  33546  mgcmnt2  33547  mgcf1olem1  33555  mgcf1olem2  33556  mgcf1o  33557  erlcl2  33815  erler  33819  mtyf2  36295  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  fourierdlem48  47133  fourierdlem76  47161  fourierdlem80  47165  fourierdlem93  47178  fourierdlem94  47179  fourierdlem104  47189  fourierdlem113  47198  mea0  47433  meaiunlelem  47447  meaiuninclem  47459  omessle  47477  omedm  47478  carageniuncllem2  47501  hspmbllem3  47607  sectpropdlem  50113  invpropdlem  50115  isopropdlem  50117  uprcl5  50269