Theorem simprld 759

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  fpwwe2lem6  9849  fpwwe2lem7  9850  fpwwe2lem9  9852  canthnumlem  9862  canthp1lem2  9867  latcl2  17510  clatlem  17573  dirtr  17698  srglz  18994  lmodvsass  19375  lmghm  19519  evlssca  20009  mircgr  26139  dfcgra2  26312  maxsta  32321  lbioc  41220  icccncfext  41600  stoweidlem37  41753  fourierdlem41  41864  fourierdlem48  41870  fourierdlem49  41871  fourierdlem74  41896  fourierdlem75  41897  salgencl  42046  salgenuni  42051  issalgend  42052  smfaddlem1  42470