Theorem simplrd 775

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  erinxp  8735  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem8  10559  lejoin2  18347  lemeet2  18361  dirdm  18564  dirref  18565  lmhmlmod2  21029  pi1cpbl  25036  pntlemr  27590  oppne2  28835  dfcgra2  28923  mgcf2  33075  mgccole2  33077  mgcmnt1  33078  mgcmnt2  33079  mgcf1olem1  33087  mgcf1olem2  33088  mgcf1o  33089  erlcl2  33349  erler  33353  mtyf2  35786  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  fourierdlem48  46604  fourierdlem76  46632  fourierdlem80  46636  fourierdlem93  46649  fourierdlem94  46650  fourierdlem104  46660  fourierdlem113  46669  mea0  46904  meaiunlelem  46918  meaiuninclem  46930  omessle  46948  omedm  46949  carageniuncllem2  46972  hspmbllem3  47078  sectpropdlem  49533  invpropdlem  49535  isopropdlem  49537  uprcl5  49689