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  10723  fpwwe2lem6  10724  fpwwe2lem8  10726  canthnumlem  10736  canthp1lem2  10741  latcl2  18615  clatlem  18681  dirtr  18781  srglz  20439  lmodvsass  21167  lmghm  21311  evlssca  22408  mircgr  29134  dfcgra2  29343  mgcmnt1d  33604  mgcmnt2d  33605  mgcf1o  33610  ssmxidllem  34044  ssmxidl  34045  maxsta  36405  lbioc  46618  icccncfext  46990  stoweidlem37  47140  fourierdlem41  47251  fourierdlem48  47257  fourierdlem49  47258  fourierdlem74  47283  fourierdlem75  47284  salgencl  47435  salgenuni  47440  issalgend  47441  smfaddlem1  47866  funcoppc4  50353  parhomne2  50847