Theorem simprld 771

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

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  canthnumlem  10561  canthp1lem2  10566  latcl2  18360  clatlem  18426  dirtr  18526  srglz  20111  lmodvsass  20808  lmghm  20953  evlssca  22012  mircgr  28620  dfcgra2  28793  mgcmnt1d  32952  mgcmnt2d  32953  mgcf1o  32958  ssmxidllem  33420  ssmxidl  33421  maxsta  35526  lbioc  45495  icccncfext  45869  stoweidlem37  46019  fourierdlem41  46130  fourierdlem48  46136  fourierdlem49  46137  fourierdlem74  46162  fourierdlem75  46163  salgencl  46314  salgenuni  46319  issalgend  46320  smfaddlem1  46745  funcoppc4  49130