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  10546  fpwwe2lem6  10547  fpwwe2lem8  10549  canthnumlem  10559  canthp1lem2  10564  latcl2  18359  clatlem  18425  dirtr  18525  srglz  20143  lmodvsass  20838  lmghm  20983  evlssca  22049  mircgr  28729  dfcgra2  28902  mgcmnt1d  33079  mgcmnt2d  33080  mgcf1o  33085  ssmxidllem  33554  ssmxidl  33555  maxsta  35748  lbioc  45759  icccncfext  46131  stoweidlem37  46281  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem74  46424  fourierdlem75  46425  salgencl  46576  salgenuni  46581  issalgend  46582  smfaddlem1  47007  funcoppc4  49389