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  10648  fpwwe2lem6  10649  fpwwe2lem8  10651  canthnumlem  10661  canthp1lem2  10666  latcl2  18530  clatlem  18596  dirtr  18696  srglz  20353  lmodvsass  21077  lmghm  21221  evlssca  22316  mircgr  29016  dfcgra2  29225  mgcmnt1d  33445  mgcmnt2d  33446  mgcf1o  33451  ssmxidllem  33884  ssmxidl  33885  maxsta  36141  lbioc  46351  icccncfext  46723  stoweidlem37  46873  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  fourierdlem74  47016  fourierdlem75  47017  salgencl  47168  salgenuni  47173  issalgend  47174  smfaddlem1  47599  funcoppc4  50078