Theorem simprld 781

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 499	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
3	2	simpld 498	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fpwwe2lem5  10590  fpwwe2lem6  10591  fpwwe2lem8  10593  canthnumlem  10603  canthp1lem2  10608  latcl2  18451  clatlem  18517  dirtr  18617  srglz  20237  lmodvsass  20934  lmghm  21078  evlssca  22127  mircgr  28803  dfcgra2  28976  mgcmnt1d  33136  mgcmnt2d  33137  mgcf1o  33142  ssmxidllem  33622  ssmxidl  33623  maxsta  35868  lbioc  46053  icccncfext  46425  stoweidlem37  46575  fourierdlem41  46686  fourierdlem48  46692  fourierdlem49  46693  fourierdlem74  46718  fourierdlem75  46719  salgencl  46870  salgenuni  46875  issalgend  46876  smfaddlem1  47301  funcoppc4  49729