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  8798  lejoin1  18463  lemeet1  18477  reldir  18680  gexdvdsi  19684  lmhmlmod1  21191  pi1cpbl  25240  hlgrcl1  28909  oppne1  29059  trgcopyeulem  29153  dfcgra2  29178  prlngrcl1  29229  subupgr  29674  3trlond  30561  3pthond  30563  3spthond  30565  grpolid  30905  mgcf1  33339  mgccole1  33341  mgcmnt1  33343  mgcmnt2  33344  mgcf1olem1  33352  mgcf1olem2  33353  mgcf1o  33354  erlcl1  33611  erler  33616  mfsdisj  36063  linethru  36666  rngoablo  38600  fourierdlem37  46899  fourierdlem48  46909  fourierdlem93  46954  fourierdlem94  46955  fourierdlem104  46965  fourierdlem112  46973  fourierdlem113  46974  dmmeasal  47207  meaf  47208  meaiuninclem  47235  omef  47251  ome0  47252  omedm  47254  hspmbllem3  47383  sectpropdlem  49855  invpropdlem  49857  isopropdlem  49859  uprcl4  50010