Theorem simplrd 770

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  8829  fpwwe2lem5  10672  fpwwe2lem6  10673  fpwwe2lem8  10675  lejoin2  18442  lemeet2  18456  dirdm  18657  dirref  18658  lmhmlmod2  21048  pi1cpbl  25090  pntlemr  27660  oppne2  28764  dfcgra2  28852  mgcf2  32963  mgccole2  32965  mgcmnt1  32966  mgcmnt2  32967  mgcf1olem1  32975  mgcf1olem2  32976  mgcf1o  32977  erlcl2  33247  erler  33251  mtyf2  35535  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  fourierdlem48  46109  fourierdlem76  46137  fourierdlem80  46141  fourierdlem93  46154  fourierdlem94  46155  fourierdlem104  46165  fourierdlem113  46174  mea0  46409  meaiunlelem  46423  meaiuninclem  46435  omessle  46453  omedm  46454  carageniuncllem2  46477  hspmbllem3  46583