Theorem simplrd 793

Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
simplrd.1	|- ( ph -> ( ( ps /\ ch ) /\ th ) )

Assertion

Ref	Expression
simplrd	|- ( ph -> ch )

Proof of Theorem simplrd

Step	Hyp	Ref	Expression
1		simplrd.1	. . 3 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
2	1	simpld 475	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simprd 479	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  dfcgra2  25721  isclwwlksng  26888  mtyf2  31448  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  fourierdlem48  40371  fourierdlem76  40399  fourierdlem80  40403  fourierdlem93  40416  fourierdlem94  40417  fourierdlem104  40427  fourierdlem113  40436  ismea  40668  mea0  40671  meaiunlelem  40685  meaiuninclem  40697  omessle  40712  omedm  40713  carageniuncllem2  40736  hspmbllem3  40842