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  8767  lejoin1  18350  lemeet1  18364  reldir  18565  gexdvdsi  19520  lmhmlmod1  20947  pi1cpbl  24951  oppne1  28675  trgcopyeulem  28739  dfcgra2  28764  subupgr  29221  3trlond  30109  3pthond  30111  3spthond  30113  grpolid  30452  mgcf1  32921  mgccole1  32923  mgcmnt1  32925  mgcmnt2  32926  mgcf1olem1  32934  mgcf1olem2  32935  mgcf1o  32936  erlcl1  33218  erler  33223  mfsdisj  35544  linethru  36148  rngoablo  37909  fourierdlem37  46149  fourierdlem48  46159  fourierdlem93  46204  fourierdlem94  46205  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  dmmeasal  46457  meaf  46458  meaiuninclem  46485  omef  46501  ome0  46502  omedm  46504  hspmbllem3  46633  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  uprcl4  49184