Theorem simplld 765

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  erinxp  8580  lejoin1  18102  lemeet1  18116  reldir  18317  gexdvdsi  19188  lmhmlmod1  20295  pi1cpbl  24207  oppne1  27102  trgcopyeulem  27166  dfcgra2  27191  subupgr  27654  3trlond  28537  3pthond  28539  3spthond  28541  grpolid  28878  mgcf1  31266  mgccole1  31268  mgcmnt1  31270  mgcmnt2  31271  mgcf1olem1  31279  mgcf1olem2  31280  mgcf1o  31281  mfsdisj  33512  linethru  34455  rngoablo  36066  fourierdlem37  43685  fourierdlem48  43695  fourierdlem93  43740  fourierdlem94  43741  fourierdlem104  43751  fourierdlem112  43759  fourierdlem113  43760  dmmeasal  43990  meaf  43991  meaiuninclem  44018  omef  44034  ome0  44035  omedm  44037  hspmbllem3  44166