Theorem simprld 795

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  srglz  18527  lmodvsass  18888  evlssca  19522  dfcgra2  25721  maxsta  31451  lbioc  39739  icccncfext  40100  stoweidlem37  40254  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem74  40397  fourierdlem75  40398  salgencl  40550  salgenuni  40555  issalgend  40556  smfaddlem1  40971