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  8814  lejoin1  18403  lemeet1  18417  reldir  18618  gexdvdsi  19574  lmhmlmod1  21005  pi1cpbl  25032  oppne1  28704  trgcopyeulem  28768  dfcgra2  28793  subupgr  29251  3trlond  30139  3pthond  30141  3spthond  30143  grpolid  30482  mgcf1  32924  mgccole1  32926  mgcmnt1  32928  mgcmnt2  32929  mgcf1olem1  32937  mgcf1olem2  32938  mgcf1o  32939  erlcl1  33210  erler  33215  mfsdisj  35496  linethru  36095  rngoablo  37856  fourierdlem37  46104  fourierdlem48  46114  fourierdlem93  46159  fourierdlem94  46160  fourierdlem104  46170  fourierdlem112  46178  fourierdlem113  46179  dmmeasal  46412  meaf  46413  meaiuninclem  46440  omef  46456  ome0  46457  omedm  46459  hspmbllem3  46588  uprcl4  48902