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  8840  lejoin1  18585  lemeet1  18599  reldir  18802  gexdvdsi  19827  lmhmlmod1  21338  pi1cpbl  25395  hlgrcl1  29096  oppne1  29247  trgcopyeulem  29342  dfcgra2  29368  tgaaddcpbllem1  29379  tgaaddcpbl  29382  cgraer  29407  angmgmlem  29425  prlngrcl1  29450  subupgr  29898  3trlond  30804  3pthond  30806  3spthond  30808  grpolid  31148  mgcf1  33619  mgccole1  33621  mgcmnt1  33623  mgcmnt2  33624  mgcf1olem1  33632  mgcf1olem2  33633  mgcf1o  33634  erlcl1  33891  erler  33896  mfsdisj  36482  linethru  37096  rngoablo  39034  fourierdlem37  47359  fourierdlem48  47369  fourierdlem93  47414  fourierdlem94  47415  fourierdlem104  47425  fourierdlem112  47433  fourierdlem113  47434  dmmeasal  47667  meaf  47668  meaiuninclem  47695  omef  47711  ome0  47712  omedm  47714  hspmbllem3  47843  sectpropdlem  50355  invpropdlem  50357  isopropdlem  50359  uprcl4  50512