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  10056  fpwwe2lem7  10057  fpwwe2lem9  10059  canthnumlem  10069  canthp1lem2  10074  latcl2  17657  clatlem  17720  dirtr  17845  srglz  19276  lmodvsass  19658  lmghm  19802  evlssca  20301  mircgr  26442  dfcgra2  26615  ssmxidllem  30978  ssmxidl  30979  maxsta  32801  lbioc  41787  icccncfext  42168  stoweidlem37  42321  fourierdlem41  42432  fourierdlem48  42438  fourierdlem49  42439  fourierdlem74  42464  fourierdlem75  42465  salgencl  42614  salgenuni  42619  issalgend  42620  smfaddlem1  43038