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  8764  lejoin1  18343  lemeet1  18357  reldir  18558  gexdvdsi  19513  lmhmlmod1  20940  pi1cpbl  24944  oppne1  28668  trgcopyeulem  28732  dfcgra2  28757  subupgr  29214  3trlond  30102  3pthond  30104  3spthond  30106  grpolid  30445  mgcf1  32914  mgccole1  32916  mgcmnt1  32918  mgcmnt2  32919  mgcf1olem1  32927  mgcf1olem2  32928  mgcf1o  32929  erlcl1  33211  erler  33216  mfsdisj  35537  linethru  36141  rngoablo  37902  fourierdlem37  46142  fourierdlem48  46152  fourierdlem93  46197  fourierdlem94  46198  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  dmmeasal  46450  meaf  46451  meaiuninclem  46478  omef  46494  ome0  46495  omedm  46497  hspmbllem3  46626  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029  uprcl4  49180