Theorem simprld 770

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fpwwe2lem6  10060  fpwwe2lem7  10061  fpwwe2lem9  10063  canthnumlem  10073  canthp1lem2  10078  latcl2  17661  clatlem  17724  dirtr  17849  srglz  19280  lmodvsass  19662  lmghm  19806  evlssca  20305  mircgr  26446  dfcgra2  26619  ssmxidllem  30982  ssmxidl  30983  maxsta  32805  lbioc  41795  icccncfext  42176  stoweidlem37  42329  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem74  42472  fourierdlem75  42473  salgencl  42622  salgenuni  42627  issalgend  42628  smfaddlem1  43046