Theorem simplld 766

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  erinxp  8371  lejoin1  17622  lemeet1  17636  reldir  17843  gexdvdsi  18708  lmhmlmod1  19805  pi1cpbl  23648  oppne1  26527  trgcopyeulem  26591  dfcgra2  26616  subupgr  27069  3trlond  27952  3pthond  27954  3spthond  27956  grpolid  28293  mfsdisj  32797  linethru  33614  rngoablo  35201  fourierdlem37  42449  fourierdlem48  42459  fourierdlem93  42504  fourierdlem94  42505  fourierdlem104  42515  fourierdlem112  42523  fourierdlem113  42524  dmmeasal  42754  meaf  42755  meaiuninclem  42782  omef  42798  ome0  42799  omedm  42801  hspmbllem3  42930