Theorem simplld 768

Description: Deduction form of simpll 767, 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  8731  lejoin1  18339  lemeet1  18353  reldir  18556  gexdvdsi  19549  lmhmlmod1  21020  pi1cpbl  25021  oppne1  28823  trgcopyeulem  28887  dfcgra2  28912  subupgr  29370  3trlond  30258  3pthond  30260  3spthond  30262  grpolid  30602  mgcf1  33063  mgccole1  33065  mgcmnt1  33067  mgcmnt2  33068  mgcf1olem1  33076  mgcf1olem2  33077  mgcf1o  33078  erlcl1  33336  erler  33341  mfsdisj  35748  linethru  36351  rngoablo  38243  fourierdlem37  46590  fourierdlem48  46600  fourierdlem93  46645  fourierdlem94  46646  fourierdlem104  46656  fourierdlem112  46664  fourierdlem113  46665  dmmeasal  46898  meaf  46899  meaiuninclem  46926  omef  46942  ome0  46943  omedm  46945  hspmbllem3  47074  sectpropdlem  49523  invpropdlem  49525  isopropdlem  49527  uprcl4  49678