Theorem simplld 775

Description: Deduction form of simpll 774, 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  8761  lejoin1  18390  lemeet1  18404  reldir  18607  gexdvdsi  19599  lmhmlmod1  21073  pi1cpbl  25079  oppne1  28880  trgcopyeulem  28944  dfcgra2  28969  subupgr  29427  3trlond  30314  3pthond  30316  3spthond  30318  grpolid  30658  mgcf1  33120  mgccole1  33122  mgcmnt1  33124  mgcmnt2  33125  mgcf1olem1  33133  mgcf1olem2  33134  mgcf1o  33135  erlcl1  33395  erler  33400  mfsdisj  35848  linethru  36451  rngoablo  38355  fourierdlem37  46666  fourierdlem48  46676  fourierdlem93  46721  fourierdlem94  46722  fourierdlem104  46732  fourierdlem112  46740  fourierdlem113  46741  dmmeasal  46974  meaf  46975  meaiuninclem  47002  omef  47018  ome0  47019  omedm  47021  hspmbllem3  47150  sectpropdlem  49605  invpropdlem  49607  isopropdlem  49609  uprcl4  49760