Theorem simprld 783

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 500	. 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:  fpwwe2lem5  10608  fpwwe2lem6  10609  fpwwe2lem8  10611  canthnumlem  10621  canthp1lem2  10626  latcl2  18482  clatlem  18548  dirtr  18648  srglz  20281  lmodvsass  20977  lmghm  21121  evlssca  22205  mircgr  28888  dfcgra2  29082  mgcmnt1d  33230  mgcmnt2d  33231  mgcf1o  33236  ssmxidllem  33673  ssmxidl  33674  maxsta  35917  lbioc  46087  icccncfext  46459  stoweidlem37  46609  fourierdlem41  46720  fourierdlem48  46726  fourierdlem49  46727  fourierdlem74  46752  fourierdlem75  46753  salgencl  46904  salgenuni  46909  issalgend  46910  smfaddlem1  47335  funcoppc4  49773