Theorem simprld 772

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  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  canthnumlem  10571  canthp1lem2  10576  latcl2  18402  clatlem  18468  dirtr  18568  srglz  20189  lmodvsass  20882  lmghm  21026  evlssca  22072  mircgr  28725  dfcgra2  28898  mgcmnt1d  33057  mgcmnt2d  33058  mgcf1o  33063  ssmxidllem  33533  ssmxidl  33534  maxsta  35736  lbioc  45943  icccncfext  46315  stoweidlem37  46465  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem74  46608  fourierdlem75  46609  salgencl  46760  salgenuni  46765  issalgend  46766  smfaddlem1  47191  funcoppc4  49619