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  8738  lejoin1  18348  lemeet1  18362  reldir  18565  gexdvdsi  19558  lmhmlmod1  21028  pi1cpbl  25011  oppne1  28809  trgcopyeulem  28873  dfcgra2  28898  subupgr  29356  3trlond  30243  3pthond  30245  3spthond  30247  grpolid  30587  mgcf1  33048  mgccole1  33050  mgcmnt1  33052  mgcmnt2  33053  mgcf1olem1  33061  mgcf1olem2  33062  mgcf1o  33063  erlcl1  33321  erler  33326  mfsdisj  35732  linethru  36335  rngoablo  38229  fourierdlem37  46572  fourierdlem48  46582  fourierdlem93  46627  fourierdlem94  46628  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  dmmeasal  46880  meaf  46881  meaiuninclem  46908  omef  46924  ome0  46925  omedm  46927  hspmbllem3  47056  sectpropdlem  49511  invpropdlem  49513  isopropdlem  49515  uprcl4  49666