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  8836  lejoin1  18448  lemeet1  18462  reldir  18663  gexdvdsi  19622  lmhmlmod1  21056  pi1cpbl  25099  oppne1  28772  trgcopyeulem  28836  dfcgra2  28861  subupgr  29327  3trlond  30215  3pthond  30217  3spthond  30219  grpolid  30558  mgcf1  32976  mgccole1  32978  mgcmnt1  32980  mgcmnt2  32981  mgcf1olem1  32989  mgcf1olem2  32990  mgcf1o  32991  erlcl1  33260  erler  33265  mfsdisj  35547  linethru  36147  rngoablo  37907  fourierdlem37  46111  fourierdlem48  46121  fourierdlem93  46166  fourierdlem94  46167  fourierdlem104  46177  fourierdlem112  46185  fourierdlem113  46186  dmmeasal  46419  meaf  46420  meaiuninclem  46447  omef  46463  ome0  46464  omedm  46466  hspmbllem3  46595