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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  fpwwe2lem5  10214  fpwwe2lem6  10215  fpwwe2lem8  10217  canthnumlem  10227  canthp1lem2  10232  latcl2  17896  clatlem  17962  dirtr  18062  srglz  19496  lmodvsass  19878  lmghm  20022  evlssca  21003  mircgr  26702  dfcgra2  26875  mgcmnt1d  30948  mgcmnt2d  30949  mgcf1o  30954  ssmxidllem  31309  ssmxidl  31310  maxsta  33183  lbioc  42667  icccncfext  43046  stoweidlem37  43196  fourierdlem41  43307  fourierdlem48  43313  fourierdlem49  43314  fourierdlem74  43339  fourierdlem75  43340  salgencl  43489  salgenuni  43494  issalgend  43495  smfaddlem1  43913