Theorem simprld 772

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  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  canthnumlem  10571  canthp1lem2  10576  latcl2  18371  clatlem  18437  dirtr  18537  srglz  20155  lmodvsass  20850  lmghm  20995  evlssca  22061  mircgr  28741  dfcgra2  28914  mgcmnt1d  33089  mgcmnt2d  33090  mgcf1o  33095  ssmxidllem  33565  ssmxidl  33566  maxsta  35767  lbioc  45867  icccncfext  46239  stoweidlem37  46389  fourierdlem41  46500  fourierdlem48  46506  fourierdlem49  46507  fourierdlem74  46532  fourierdlem75  46533  salgencl  46684  salgenuni  46689  issalgend  46690  smfaddlem1  47115  funcoppc4  49497