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  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  canthnumlem  10608  canthp1lem2  10613  latcl2  18402  clatlem  18468  dirtr  18568  srglz  20124  lmodvsass  20800  lmghm  20945  evlssca  22003  mircgr  28591  dfcgra2  28764  mgcmnt1d  32930  mgcmnt2d  32931  mgcf1o  32936  ssmxidllem  33451  ssmxidl  33452  maxsta  35548  lbioc  45518  icccncfext  45892  stoweidlem37  46042  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem74  46185  fourierdlem75  46186  salgencl  46337  salgenuni  46342  issalgend  46343  smfaddlem1  46768  funcoppc4  49137