Theorem simprld 783

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem8  10624  canthnumlem  10634  canthp1lem2  10639  latcl2  18493  clatlem  18559  dirtr  18659  srglz  20291  lmodvsass  20989  lmghm  21133  evlssca  22226  mircgr  28912  dfcgra2  29119  mgcmnt1d  33295  mgcmnt2d  33296  mgcf1o  33301  ssmxidllem  33734  ssmxidl  33735  maxsta  36024  lbioc  46209  icccncfext  46581  stoweidlem37  46731  fourierdlem41  46842  fourierdlem48  46848  fourierdlem49  46849  fourierdlem74  46874  fourierdlem75  46875  salgencl  47026  salgenuni  47031  issalgend  47032  smfaddlem1  47457  funcoppc4  49899