Theorem simprld 769

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fpwwe2lem5  10391  fpwwe2lem6  10392  fpwwe2lem8  10394  canthnumlem  10404  canthp1lem2  10409  latcl2  18154  clatlem  18220  dirtr  18320  srglz  19763  lmodvsass  20148  lmghm  20293  evlssca  21299  mircgr  27018  dfcgra2  27191  mgcmnt1d  31275  mgcmnt2d  31276  mgcf1o  31281  ssmxidllem  31641  ssmxidl  31642  maxsta  33516  lbioc  43051  icccncfext  43428  stoweidlem37  43578  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem74  43721  fourierdlem75  43722  salgencl  43871  salgenuni  43876  issalgend  43877  smfaddlem1  44298