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  8715  lejoin1  18285  lemeet1  18299  reldir  18502  gexdvdsi  19493  lmhmlmod1  20965  pi1cpbl  24969  oppne1  28717  trgcopyeulem  28781  dfcgra2  28806  subupgr  29263  3trlond  30148  3pthond  30150  3spthond  30152  grpolid  30491  mgcf1  32964  mgccole1  32966  mgcmnt1  32968  mgcmnt2  32969  mgcf1olem1  32977  mgcf1olem2  32978  mgcf1o  32979  erlcl1  33222  erler  33227  mfsdisj  35582  linethru  36186  rngoablo  37947  fourierdlem37  46181  fourierdlem48  46191  fourierdlem93  46236  fourierdlem94  46237  fourierdlem104  46247  fourierdlem112  46255  fourierdlem113  46256  dmmeasal  46489  meaf  46490  meaiuninclem  46517  omef  46533  ome0  46534  omedm  46536  hspmbllem3  46665  sectpropdlem  49067  invpropdlem  49069  isopropdlem  49071  uprcl4  49222