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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  erinxp  8354  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  lejoin2  17615  lemeet2  17629  dirdm  17836  dirref  17837  lmhmlmod2  19797  pi1cpbl  23649  pntlemr  26186  oppne2  26536  dfcgra2  26624  mgcf2  30697  mgccole2  30699  mcgmnt1  30700  mcgmnt2  30701  mtyf2  32911  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  fourierdlem48  42796  fourierdlem76  42824  fourierdlem80  42828  fourierdlem93  42841  fourierdlem94  42842  fourierdlem104  42852  fourierdlem113  42861  mea0  43093  meaiunlelem  43107  meaiuninclem  43119  omessle  43137  omedm  43138  carageniuncllem2  43161  hspmbllem3  43267