Theorem simplld 767

Description: Deduction form of simpll 766, 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 210  df-an 400

This theorem is referenced by:  erinxp  8354  lejoin1  17614  lemeet1  17628  reldir  17835  gexdvdsi  18700  lmhmlmod1  19798  pi1cpbl  23649  oppne1  26535  trgcopyeulem  26599  dfcgra2  26624  subupgr  27077  3trlond  27958  3pthond  27960  3spthond  27962  grpolid  28299  mgcf1  30696  mgccole1  30698  mcgmnt1  30700  mcgmnt2  30701  mfsdisj  32910  linethru  33727  rngoablo  35346  fourierdlem37  42786  fourierdlem48  42796  fourierdlem93  42841  fourierdlem94  42842  fourierdlem104  42852  fourierdlem112  42860  fourierdlem113  42861  dmmeasal  43091  meaf  43092  meaiuninclem  43119  omef  43135  ome0  43136  omedm  43138  hspmbllem3  43267