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  10533  fpwwe2lem6  10534  fpwwe2lem8  10536  canthnumlem  10546  canthp1lem2  10551  latcl2  18344  clatlem  18410  dirtr  18510  srglz  20128  lmodvsass  20822  lmghm  20967  evlssca  22025  mircgr  28636  dfcgra2  28809  mgcmnt1d  32985  mgcmnt2d  32986  mgcf1o  32991  ssmxidllem  33445  ssmxidl  33446  maxsta  35619  lbioc  45637  icccncfext  46009  stoweidlem37  46159  fourierdlem41  46270  fourierdlem48  46276  fourierdlem49  46277  fourierdlem74  46302  fourierdlem75  46303  salgencl  46454  salgenuni  46459  issalgend  46460  smfaddlem1  46885  funcoppc4  49269