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  10701  fpwwe2lem6  10702  fpwwe2lem8  10704  canthnumlem  10714  canthp1lem2  10719  latcl2  18590  clatlem  18656  dirtr  18756  srglz  20414  lmodvsass  21142  lmghm  21286  evlssca  22383  mircgr  29111  dfcgra2  29320  mgcmnt1d  33540  mgcmnt2d  33541  mgcf1o  33546  ssmxidllem  33980  ssmxidl  33981  maxsta  36288  lbioc  46469  icccncfext  46841  stoweidlem37  46991  fourierdlem41  47102  fourierdlem48  47108  fourierdlem49  47109  fourierdlem74  47134  fourierdlem75  47135  salgencl  47286  salgenuni  47291  issalgend  47292  smfaddlem1  47717  funcoppc4  50196