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  10673  fpwwe2lem6  10674  fpwwe2lem8  10676  canthnumlem  10686  canthp1lem2  10691  latcl2  18494  clatlem  18560  dirtr  18660  srglz  20226  lmodvsass  20902  lmghm  21048  evlssca  22131  mircgr  28680  dfcgra2  28853  mgcmnt1d  32972  mgcmnt2d  32973  mgcf1o  32978  ssmxidllem  33481  ssmxidl  33482  maxsta  35539  lbioc  45466  icccncfext  45843  stoweidlem37  45993  fourierdlem41  46104  fourierdlem48  46110  fourierdlem49  46111  fourierdlem74  46136  fourierdlem75  46137  salgencl  46288  salgenuni  46293  issalgend  46294  smfaddlem1  46719