Theorem simplld 767

Description: Deduction form of simpll 766, 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  8768  lejoin1  18349  lemeet1  18363  reldir  18564  gexdvdsi  19519  lmhmlmod1  20946  pi1cpbl  24950  oppne1  28675  trgcopyeulem  28739  dfcgra2  28764  subupgr  29221  3trlond  30109  3pthond  30111  3spthond  30113  grpolid  30452  mgcf1  32922  mgccole1  32924  mgcmnt1  32926  mgcmnt2  32927  mgcf1olem1  32935  mgcf1olem2  32936  mgcf1o  32937  erlcl1  33219  erler  33224  mfsdisj  35539  linethru  36138  rngoablo  37899  fourierdlem37  46115  fourierdlem48  46125  fourierdlem93  46170  fourierdlem94  46171  fourierdlem104  46181  fourierdlem112  46189  fourierdlem113  46190  dmmeasal  46423  meaf  46424  meaiuninclem  46451  omef  46467  ome0  46468  omedm  46470  hspmbllem3  46599  sectpropdlem  48953  invpropdlem  48955  isopropdlem  48957  uprcl4  49098