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  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  canthnumlem  10562  canthp1lem2  10567  latcl2  18393  clatlem  18459  dirtr  18559  srglz  20180  lmodvsass  20873  lmghm  21018  evlssca  22082  mircgr  28739  dfcgra2  28912  mgcmnt1d  33072  mgcmnt2d  33073  mgcf1o  33078  ssmxidllem  33548  ssmxidl  33549  maxsta  35752  lbioc  45961  icccncfext  46333  stoweidlem37  46483  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem74  46626  fourierdlem75  46627  salgencl  46778  salgenuni  46783  issalgend  46784  smfaddlem1  47209  funcoppc4  49631