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  8740  lejoin1  18317  lemeet1  18331  reldir  18534  gexdvdsi  19524  lmhmlmod1  20997  pi1cpbl  25012  oppne1  28825  trgcopyeulem  28889  dfcgra2  28914  subupgr  29372  3trlond  30260  3pthond  30262  3spthond  30264  grpolid  30603  mgcf1  33080  mgccole1  33082  mgcmnt1  33084  mgcmnt2  33085  mgcf1olem1  33093  mgcf1olem2  33094  mgcf1o  33095  erlcl1  33353  erler  33358  mfsdisj  35763  linethru  36366  rngoablo  38153  fourierdlem37  46496  fourierdlem48  46506  fourierdlem93  46551  fourierdlem94  46552  fourierdlem104  46562  fourierdlem112  46570  fourierdlem113  46571  dmmeasal  46804  meaf  46805  meaiuninclem  46832  omef  46848  ome0  46849  omedm  46851  hspmbllem3  46980  sectpropdlem  49389  invpropdlem  49391  isopropdlem  49393  uprcl4  49544