Theorem simplld 779

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

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  erinxp  8777  lejoin1  18428  lemeet1  18442  reldir  18645  gexdvdsi  19644  lmhmlmod1  21123  pi1cpbl  25164  oppne1  28972  trgcopyeulem  29057  dfcgra2  29082  subupgr  29546  3trlond  30433  3pthond  30435  3spthond  30437  grpolid  30777  mgcf1  33221  mgccole1  33223  mgcmnt1  33225  mgcmnt2  33226  mgcf1olem1  33234  mgcf1olem2  33235  mgcf1o  33236  erlcl1  33493  erler  33498  mfsdisj  35913  linethru  36516  rngoablo  38419  fourierdlem37  46716  fourierdlem48  46726  fourierdlem93  46771  fourierdlem94  46772  fourierdlem104  46782  fourierdlem112  46790  fourierdlem113  46791  dmmeasal  47024  meaf  47025  meaiuninclem  47052  omef  47068  ome0  47069  omedm  47071  hspmbllem3  47200  sectpropdlem  49665  invpropdlem  49667  isopropdlem  49669  uprcl4  49820