Theorem simplld 787

Description: Deduction form of simpll 786, 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 474	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 474	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  lejoin1  16835  lemeet1  16849  reldir  17056  gexdvdsi  17821  lmhmlmod1  18854  oppne1  25433  trgcopyeulem  25497  dfcgra2  25521  constr3cyclp  26190  grpolid  26754  mfsdisj  30701  linethru  31430  rngoablo  32877  fourierdlem37  39037  fourierdlem48  39047  fourierdlem93  39092  fourierdlem94  39093  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  ismea  39344  dmmeasal  39345  meaf  39346  meaiuninclem  39373  omef  39386  ome0  39387  omedm  39389  hspmbllem3  39518  subupgr  40511  3trlond  41340  3pthond  41342  3spthond  41344