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 496	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 496	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  erinxp  8785  lejoin1  18337  lemeet1  18351  reldir  18552  gexdvdsi  19451  lmhmlmod1  20644  pi1cpbl  24560  oppne1  27992  trgcopyeulem  28056  dfcgra2  28081  subupgr  28544  3trlond  29426  3pthond  29428  3spthond  29430  grpolid  29769  mgcf1  32158  mgccole1  32160  mgcmnt1  32162  mgcmnt2  32163  mgcf1olem1  32171  mgcf1olem2  32172  mgcf1o  32173  mfsdisj  34541  linethru  35125  rngoablo  36776  fourierdlem37  44860  fourierdlem48  44870  fourierdlem93  44915  fourierdlem94  44916  fourierdlem104  44926  fourierdlem112  44934  fourierdlem113  44935  dmmeasal  45168  meaf  45169  meaiuninclem  45196  omef  45212  ome0  45213  omedm  45215  hspmbllem3  45344