Theorem simprld 771

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fpwwe2lem5  10523  fpwwe2lem6  10524  fpwwe2lem8  10526  canthnumlem  10536  canthp1lem2  10541  latcl2  18339  clatlem  18405  dirtr  18505  srglz  20124  lmodvsass  20818  lmghm  20963  evlssca  22022  mircgr  28633  dfcgra2  28806  mgcmnt1d  32973  mgcmnt2d  32974  mgcf1o  32979  ssmxidllem  33433  ssmxidl  33434  maxsta  35586  lbioc  45552  icccncfext  45924  stoweidlem37  46074  fourierdlem41  46185  fourierdlem48  46191  fourierdlem49  46192  fourierdlem74  46217  fourierdlem75  46218  salgencl  46369  salgenuni  46374  issalgend  46375  smfaddlem1  46800  funcoppc4  49175