Theorem simplld 780

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  erinxp  8795  lejoin1  18476  lemeet1  18490  reldir  18693  gexdvdsi  19716  lmhmlmod1  21223  pi1cpbl  25278  hlgrcl1  28953  oppne1  29104  trgcopyeulem  29199  dfcgra2  29225  tgaaddcpbllem1  29236  tgaaddcpbl  29239  cgraer  29264  angmgmlem  29282  prlngrcl1  29307  subupgr  29755  3trlond  30661  3pthond  30663  3spthond  30665  grpolid  31005  mgcf1  33436  mgccole1  33438  mgcmnt1  33440  mgcmnt2  33441  mgcf1olem1  33449  mgcf1olem2  33450  mgcf1o  33451  erlcl1  33708  erler  33713  mfsdisj  36137  linethru  36741  rngoablo  38666  fourierdlem37  46980  fourierdlem48  46990  fourierdlem93  47035  fourierdlem94  47036  fourierdlem104  47046  fourierdlem112  47054  fourierdlem113  47055  dmmeasal  47288  meaf  47289  meaiuninclem  47316  omef  47332  ome0  47333  omedm  47335  hspmbllem3  47464  sectpropdlem  49970  invpropdlem  49972  isopropdlem  49974  uprcl4  50125