Theorem simplrd 769

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  erinxp  8767  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  lejoin2  18351  lemeet2  18365  dirdm  18566  dirref  18567  lmhmlmod2  20946  pi1cpbl  24951  pntlemr  27520  oppne2  28676  dfcgra2  28764  mgcf2  32922  mgccole2  32924  mgcmnt1  32925  mgcmnt2  32926  mgcf1olem1  32934  mgcf1olem2  32935  mgcf1o  32936  erlcl2  33219  erler  33223  mtyf2  35545  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  fourierdlem48  46159  fourierdlem76  46187  fourierdlem80  46191  fourierdlem93  46204  fourierdlem94  46205  fourierdlem104  46215  fourierdlem113  46224  mea0  46459  meaiunlelem  46473  meaiuninclem  46485  omessle  46503  omedm  46504  carageniuncllem2  46527  hspmbllem3  46633  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  uprcl5  49185