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  8815  lejoin1  18561  lemeet1  18575  reldir  18778  gexdvdsi  19802  lmhmlmod1  21313  pi1cpbl  25370  hlgrcl1  29071  oppne1  29222  trgcopyeulem  29317  dfcgra2  29343  tgaaddcpbllem1  29354  tgaaddcpbl  29357  cgraer  29382  angmgmlem  29400  prlngrcl1  29425  subupgr  29873  3trlond  30779  3pthond  30781  3spthond  30783  grpolid  31123  mgcf1  33595  mgccole1  33597  mgcmnt1  33599  mgcmnt2  33600  mgcf1olem1  33608  mgcf1olem2  33609  mgcf1o  33610  erlcl1  33867  erler  33872  mfsdisj  36401  linethru  37010  rngoablo  38935  fourierdlem37  47247  fourierdlem48  47257  fourierdlem93  47302  fourierdlem94  47303  fourierdlem104  47313  fourierdlem112  47321  fourierdlem113  47322  dmmeasal  47555  meaf  47556  meaiuninclem  47583  omef  47599  ome0  47600  omedm  47602  hspmbllem3  47731  sectpropdlem  50243  invpropdlem  50245  isopropdlem  50247  uprcl4  50400