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  10750  fpwwe2lem6  10751  fpwwe2lem8  10753  canthnumlem  10763  canthp1lem2  10768  latcl2  18642  clatlem  18708  dirtr  18808  srglz  20467  lmodvsass  21195  lmghm  21339  evlssca  22436  mircgr  29162  dfcgra2  29371  mgcmnt1d  33634  mgcmnt2d  33635  mgcf1o  33640  edompidlem  33940  ssmxidllem  34082  ssmxidl  34083  maxsta  36499  lbioc  46740  icccncfext  47112  stoweidlem37  47262  fourierdlem41  47373  fourierdlem48  47379  fourierdlem49  47380  fourierdlem74  47405  fourierdlem75  47406  salgencl  47557  salgenuni  47562  issalgend  47563  smfaddlem1  47988  funcoppc4  50475  parhomne2  50969