Theorem simplld 777

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  erinxp  8768  lejoin1  18397  lemeet1  18411  reldir  18614  gexdvdsi  19606  lmhmlmod1  21080  pi1cpbl  25086  oppne1  28887  trgcopyeulem  28951  dfcgra2  28976  subupgr  29434  3trlond  30321  3pthond  30323  3spthond  30325  grpolid  30665  mgcf1  33127  mgccole1  33129  mgcmnt1  33131  mgcmnt2  33132  mgcf1olem1  33140  mgcf1olem2  33141  mgcf1o  33142  erlcl1  33402  erler  33407  mfsdisj  35864  linethru  36467  rngoablo  38371  fourierdlem37  46682  fourierdlem48  46692  fourierdlem93  46737  fourierdlem94  46738  fourierdlem104  46748  fourierdlem112  46756  fourierdlem113  46757  dmmeasal  46990  meaf  46991  meaiuninclem  47018  omef  47034  ome0  47035  omedm  47037  hspmbllem3  47166  sectpropdlem  49621  invpropdlem  49623  isopropdlem  49625  uprcl4  49776