Theorem simplld 766

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  erinxp  8373  lejoin1  17624  lemeet1  17638  reldir  17845  gexdvdsi  18710  lmhmlmod1  19807  pi1cpbl  23650  oppne1  26529  trgcopyeulem  26593  dfcgra2  26618  subupgr  27071  3trlond  27954  3pthond  27956  3spthond  27958  grpolid  28295  mfsdisj  32799  linethru  33616  rngoablo  35188  fourierdlem37  42436  fourierdlem48  42446  fourierdlem93  42491  fourierdlem94  42492  fourierdlem104  42502  fourierdlem112  42510  fourierdlem113  42511  dmmeasal  42741  meaf  42742  meaiuninclem  42769  omef  42785  ome0  42786  omedm  42788  hspmbllem3  42917