Theorem simprld 784

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fpwwe2lem5  10638  fpwwe2lem6  10639  fpwwe2lem8  10641  canthnumlem  10651  canthp1lem2  10656  latcl2  18517  clatlem  18583  dirtr  18683  srglz  20321  lmodvsass  21045  lmghm  21189  evlssca  22282  mircgr  28971  dfcgra2  29178  mgcmnt1d  33348  mgcmnt2d  33349  mgcf1o  33354  ssmxidllem  33787  ssmxidl  33788  maxsta  36067  lbioc  46270  icccncfext  46642  stoweidlem37  46792  fourierdlem41  46903  fourierdlem48  46909  fourierdlem49  46910  fourierdlem74  46935  fourierdlem75  46936  salgencl  47087  salgenuni  47092  issalgend  47093  smfaddlem1  47518  funcoppc4  49963