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 494	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 494	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  erinxp  8851  lejoin1  18456  lemeet1  18470  reldir  18671  gexdvdsi  19627  lmhmlmod1  21057  pi1cpbl  25098  oppne1  28769  trgcopyeulem  28833  dfcgra2  28858  subupgr  29324  3trlond  30207  3pthond  30209  3spthond  30211  grpolid  30550  mgcf1  32963  mgccole1  32965  mgcmnt1  32967  mgcmnt2  32968  mgcf1olem1  32976  mgcf1olem2  32977  mgcf1o  32978  erlcl1  33234  erler  33239  mfsdisj  35520  linethru  36119  rngoablo  37870  fourierdlem37  46067  fourierdlem48  46077  fourierdlem93  46122  fourierdlem94  46123  fourierdlem104  46133  fourierdlem112  46141  fourierdlem113  46142  dmmeasal  46375  meaf  46376  meaiuninclem  46403  omef  46419  ome0  46420  omedm  46422  hspmbllem3  46551