Theorem simplrd 757

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  erinxp  8163  fpwwe2lem6  9847  fpwwe2lem7  9848  fpwwe2lem9  9850  lejoin2  17471  lemeet2  17485  dirdm  17692  dirref  17693  lmhmlmod2  19516  pi1cpbl  23341  pntlemr  25870  oppne2  26220  dfcgra2  26308  mtyf2  32258  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  fourierdlem48  41816  fourierdlem76  41844  fourierdlem80  41848  fourierdlem93  41861  fourierdlem94  41862  fourierdlem104  41872  fourierdlem113  41881  mea0  42113  meaiunlelem  42127  meaiuninclem  42139  omessle  42157  omedm  42158  carageniuncllem2  42181  hspmbllem3  42287