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  45755  icccncfext  46127  stoweidlem37  46277  fourierdlem41  46388  fourierdlem48  46394  fourierdlem49  46395  fourierdlem74  46420  fourierdlem75  46421  salgencl  46572  salgenuni  46577  issalgend  46578  smfaddlem1  47003  funcoppc4  49385