Theorem simprld 777

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem8  10559  canthnumlem  10569  canthp1lem2  10574  latcl2  18400  clatlem  18466  dirtr  18566  srglz  20187  lmodvsass  20884  lmghm  21028  evlssca  22077  mircgr  28750  dfcgra2  28923  mgcmnt1d  33083  mgcmnt2d  33084  mgcf1o  33089  ssmxidllem  33563  ssmxidl  33564  maxsta  35789  lbioc  45965  icccncfext  46337  stoweidlem37  46487  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem74  46630  fourierdlem75  46631  salgencl  46782  salgenuni  46787  issalgend  46788  smfaddlem1  47213  funcoppc4  49641