Theorem simplrd 768

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  erinxp  8810  fpwwe2lem5  10660  fpwwe2lem6  10661  fpwwe2lem8  10663  lejoin2  18380  lemeet2  18394  dirdm  18595  dirref  18596  lmhmlmod2  20929  pi1cpbl  25015  pntlemr  27580  oppne2  28618  dfcgra2  28706  mgcf2  32805  mgccole2  32807  mgcmnt1  32808  mgcmnt2  32809  mgcf1olem1  32817  mgcf1olem2  32818  mgcf1o  32819  erlcl2  33051  erler  33055  mtyf2  35289  ioodvbdlimc1lem2  45455  ioodvbdlimc2lem  45457  fourierdlem48  45677  fourierdlem76  45705  fourierdlem80  45709  fourierdlem93  45722  fourierdlem94  45723  fourierdlem104  45733  fourierdlem113  45742  mea0  45977  meaiunlelem  45991  meaiuninclem  46003  omessle  46021  omedm  46022  carageniuncllem2  46045  hspmbllem3  46151