Theorem simplld 779

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  erinxp  8790  lejoin1  18439  lemeet1  18453  reldir  18656  gexdvdsi  19654  lmhmlmod1  21135  pi1cpbl  25184  hlgrcl1  28850  oppne1  29000  trgcopyeulem  29094  dfcgra2  29119  prlngrcl1  29170  subupgr  29615  3trlond  30502  3pthond  30504  3spthond  30506  grpolid  30846  mgcf1  33286  mgccole1  33288  mgcmnt1  33290  mgcmnt2  33291  mgcf1olem1  33299  mgcf1olem2  33300  mgcf1o  33301  erlcl1  33558  erler  33563  mfsdisj  36020  linethru  36623  rngoablo  38537  fourierdlem37  46838  fourierdlem48  46848  fourierdlem93  46893  fourierdlem94  46894  fourierdlem104  46904  fourierdlem112  46912  fourierdlem113  46913  dmmeasal  47146  meaf  47147  meaiuninclem  47174  omef  47190  ome0  47191  omedm  47193  hspmbllem3  47322  sectpropdlem  49791  invpropdlem  49793  isopropdlem  49795  uprcl4  49946