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  8721  lejoin1  18290  lemeet1  18304  reldir  18507  gexdvdsi  19497  lmhmlmod1  20969  pi1cpbl  24972  oppne1  28720  trgcopyeulem  28784  dfcgra2  28809  subupgr  29267  3trlond  30155  3pthond  30157  3spthond  30159  grpolid  30498  mgcf1  32976  mgccole1  32978  mgcmnt1  32980  mgcmnt2  32981  mgcf1olem1  32989  mgcf1olem2  32990  mgcf1o  32991  erlcl1  33234  erler  33239  mfsdisj  35615  linethru  36218  rngoablo  37968  fourierdlem37  46266  fourierdlem48  46276  fourierdlem93  46321  fourierdlem94  46322  fourierdlem104  46332  fourierdlem112  46340  fourierdlem113  46341  dmmeasal  46574  meaf  46575  meaiuninclem  46602  omef  46618  ome0  46619  omedm  46621  hspmbllem3  46750  sectpropdlem  49161  invpropdlem  49163  isopropdlem  49165  uprcl4  49316