Theorem simprld 768

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

This theorem is referenced by:  fpwwe2lem5  10322  fpwwe2lem6  10323  fpwwe2lem8  10325  canthnumlem  10335  canthp1lem2  10340  latcl2  18069  clatlem  18135  dirtr  18235  srglz  19678  lmodvsass  20063  lmghm  20208  evlssca  21209  mircgr  26922  dfcgra2  27095  mgcmnt1d  31177  mgcmnt2d  31178  mgcf1o  31183  ssmxidllem  31543  ssmxidl  31544  maxsta  33416  lbioc  42941  icccncfext  43318  stoweidlem37  43468  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem74  43611  fourierdlem75  43612  salgencl  43761  salgenuni  43766  issalgend  43767  smfaddlem1  44185