Theorem simplld 754

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

Hypothesis

Ref	Expression
simplld.1

Assertion

Ref	Expression
simplld

Proof of Theorem simplld

Step	Hyp	Ref	Expression
1		simplld.1	. . 3
2	1	simpld 459	. 2
3	2	simpld 459	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  lejoin1  15642  lemeet1  15656  reldir  15863  gexdvdsi  16603  lmhmlmod1  17679  oppne1  24114  opphllem4  24122  constr3cyclp  24662  grpolid  25221  rngoablo  25391  mfsdisj  28910  linethru  29803  fourierdlem37  31926  fourierdlem48  31937  fourierdlem93  31982  fourierdlem94  31983  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002

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 185  df-an 371