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  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  canthnumlem  10601  canthp1lem2  10606  latcl2  18395  clatlem  18461  dirtr  18561  srglz  20117  lmodvsass  20793  lmghm  20938  evlssca  21996  mircgr  28584  dfcgra2  28757  mgcmnt1d  32923  mgcmnt2d  32924  mgcf1o  32929  ssmxidllem  33444  ssmxidl  33445  maxsta  35541  lbioc  45511  icccncfext  45885  stoweidlem37  46035  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem74  46178  fourierdlem75  46179  salgencl  46330  salgenuni  46335  issalgend  46336  smfaddlem1  46761  funcoppc4  49133