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  8796  lejoin1  18536  lemeet1  18550  reldir  18753  gexdvdsi  19777  lmhmlmod1  21288  pi1cpbl  25345  hlgrcl1  29048  oppne1  29199  trgcopyeulem  29294  dfcgra2  29320  tgaaddcpbllem1  29331  tgaaddcpbl  29334  cgraer  29359  angmgmlem  29377  prlngrcl1  29402  subupgr  29850  3trlond  30756  3pthond  30758  3spthond  30760  grpolid  31100  mgcf1  33531  mgccole1  33533  mgcmnt1  33535  mgcmnt2  33536  mgcf1olem1  33544  mgcf1olem2  33545  mgcf1o  33546  erlcl1  33803  erler  33808  mfsdisj  36284  linethru  36888  rngoablo  38810  fourierdlem37  47098  fourierdlem48  47108  fourierdlem93  47153  fourierdlem94  47154  fourierdlem104  47164  fourierdlem112  47172  fourierdlem113  47173  dmmeasal  47406  meaf  47407  meaiuninclem  47434  omef  47450  ome0  47451  omedm  47453  hspmbllem3  47582  sectpropdlem  50088  invpropdlem  50090  isopropdlem  50092  uprcl4  50243