Theorem simprld 784

Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
simprld.1	⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simprld	⊢ (𝜑 → 𝜒)

Proof of Theorem simprld

Step	Hyp	Ref	Expression
1		simprld.1	. . 3 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
2	1	simprd 501	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
3	2	simpld 500	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fpwwe2lem5  10720  fpwwe2lem6  10721  fpwwe2lem8  10723  canthnumlem  10733  canthp1lem2  10738  latcl2  18610  clatlem  18676  dirtr  18776  srglz  20434  lmodvsass  21162  lmghm  21306  evlssca  22403  mircgr  29129  dfcgra2  29338  mgcmnt1d  33558  mgcmnt2d  33559  mgcf1o  33564  ssmxidllem  33998  ssmxidl  33999  maxsta  36319  lbioc  46525  icccncfext  46897  stoweidlem37  47047  fourierdlem41  47158  fourierdlem48  47164  fourierdlem49  47165  fourierdlem74  47190  fourierdlem75  47191  salgencl  47342  salgenuni  47347  issalgend  47348  smfaddlem1  47773  funcoppc4  50252