Theorem simplld 767

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  erinxp  8725  lejoin1  18306  lemeet1  18320  reldir  18523  gexdvdsi  19480  lmhmlmod1  20955  pi1cpbl  24960  oppne1  28704  trgcopyeulem  28768  dfcgra2  28793  subupgr  29250  3trlond  30135  3pthond  30137  3spthond  30139  grpolid  30478  mgcf1  32943  mgccole1  32945  mgcmnt1  32947  mgcmnt2  32948  mgcf1olem1  32956  mgcf1olem2  32957  mgcf1o  32958  erlcl1  33210  erler  33215  mfsdisj  35522  linethru  36126  rngoablo  37887  fourierdlem37  46126  fourierdlem48  46136  fourierdlem93  46181  fourierdlem94  46182  fourierdlem104  46192  fourierdlem112  46200  fourierdlem113  46201  dmmeasal  46434  meaf  46435  meaiuninclem  46462  omef  46478  ome0  46479  omedm  46481  hspmbllem3  46610  sectpropdlem  49022  invpropdlem  49024  isopropdlem  49026  uprcl4  49177