Theorem simplld 791

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

Hypothesis

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

Assertion

Ref	Expression
simplld	|- ( ph -> ps )

Proof of Theorem simplld

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

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:  lejoin1  17012  lemeet1  17026  reldir  17233  gexdvdsi  17998  lmhmlmod1  19033  oppne1  25633  trgcopyeulem  25697  dfcgra2  25721  subupgr  26179  3trlond  27033  3pthond  27035  3spthond  27037  grpolid  27370  mfsdisj  31447  linethru  32260  rngoablo  33707  fourierdlem37  40361  fourierdlem48  40371  fourierdlem93  40416  fourierdlem94  40417  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  ismea  40668  dmmeasal  40669  meaf  40670  meaiuninclem  40697  omef  40710  ome0  40711  omedm  40713  hspmbllem3  40842