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  8728  lejoin1  18305  lemeet1  18319  reldir  18522  gexdvdsi  19512  lmhmlmod1  20985  pi1cpbl  25000  oppne1  28813  trgcopyeulem  28877  dfcgra2  28902  subupgr  29360  3trlond  30248  3pthond  30250  3spthond  30252  grpolid  30591  mgcf1  33070  mgccole1  33072  mgcmnt1  33074  mgcmnt2  33075  mgcf1olem1  33083  mgcf1olem2  33084  mgcf1o  33085  erlcl1  33342  erler  33347  mfsdisj  35744  linethru  36347  rngoablo  38105  fourierdlem37  46384  fourierdlem48  46394  fourierdlem93  46439  fourierdlem94  46440  fourierdlem104  46450  fourierdlem112  46458  fourierdlem113  46459  dmmeasal  46692  meaf  46693  meaiuninclem  46720  omef  46736  ome0  46737  omedm  46739  hspmbllem3  46868  sectpropdlem  49277  invpropdlem  49279  isopropdlem  49281  uprcl4  49432