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  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  canthnumlem  10717  canthp1lem2  10722  latcl2  18506  clatlem  18572  dirtr  18672  srglz  20235  lmodvsass  20907  lmghm  21053  evlssca  22136  mircgr  28683  dfcgra2  28856  mgcmnt1d  32970  mgcmnt2d  32971  mgcf1o  32976  ssmxidllem  33466  ssmxidl  33467  maxsta  35522  lbioc  45431  icccncfext  45808  stoweidlem37  45958  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem74  46101  fourierdlem75  46102  salgencl  46253  salgenuni  46258  issalgend  46259  smfaddlem1  46684