Theorem simplld 784

Description: Deduction form of simpll 783, 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 490	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 490	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  erinxp  8086  lejoin1  17365  lemeet1  17379  reldir  17586  gexdvdsi  18349  lmhmlmod1  19392  pi1cpbl  23213  oppne1  26050  trgcopyeulem  26114  dfcgra2  26138  subupgr  26584  3trlond  27538  3pthond  27540  3spthond  27542  grpolid  27915  mfsdisj  31982  linethru  32788  rngoablo  34242  fourierdlem37  41148  fourierdlem48  41158  fourierdlem93  41203  fourierdlem94  41204  fourierdlem104  41214  fourierdlem112  41222  fourierdlem113  41223  ismea  41452  dmmeasal  41453  meaf  41454  meaiuninclem  41481  omef  41497  ome0  41498  omedm  41500  hspmbllem3  41629