Theorem simplld 773

Description: Deduction form of simpll 772, 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 495	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 495	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  erinxp  8735  lejoin1  18346  lemeet1  18360  reldir  18563  gexdvdsi  19556  lmhmlmod1  21030  pi1cpbl  25036  oppne1  28834  trgcopyeulem  28898  dfcgra2  28923  subupgr  29381  3trlond  30268  3pthond  30270  3spthond  30272  grpolid  30612  mgcf1  33074  mgccole1  33076  mgcmnt1  33078  mgcmnt2  33079  mgcf1olem1  33087  mgcf1olem2  33088  mgcf1o  33089  erlcl1  33348  erler  33353  mfsdisj  35785  linethru  36388  rngoablo  38282  fourierdlem37  46594  fourierdlem48  46604  fourierdlem93  46649  fourierdlem94  46650  fourierdlem104  46660  fourierdlem112  46668  fourierdlem113  46669  dmmeasal  46902  meaf  46903  meaiuninclem  46930  omef  46946  ome0  46947  omedm  46949  hspmbllem3  47078  sectpropdlem  49533  invpropdlem  49535  isopropdlem  49537  uprcl4  49688