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  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  canthnumlem  10688  canthp1lem2  10693  latcl2  18481  clatlem  18547  dirtr  18647  srglz  20205  lmodvsass  20885  lmghm  21030  evlssca  22113  mircgr  28665  dfcgra2  28838  mgcmnt1d  32987  mgcmnt2d  32988  mgcf1o  32993  ssmxidllem  33501  ssmxidl  33502  maxsta  35559  lbioc  45526  icccncfext  45902  stoweidlem37  46052  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem74  46195  fourierdlem75  46196  salgencl  46347  salgenuni  46352  issalgend  46353  smfaddlem1  46778