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  10649  fpwwe2lem6  10650  fpwwe2lem8  10652  canthnumlem  10662  canthp1lem2  10667  latcl2  18446  clatlem  18512  dirtr  18612  srglz  20168  lmodvsass  20844  lmghm  20989  evlssca  22047  mircgr  28636  dfcgra2  28809  mgcmnt1d  32977  mgcmnt2d  32978  mgcf1o  32983  ssmxidllem  33488  ssmxidl  33489  maxsta  35576  lbioc  45542  icccncfext  45916  stoweidlem37  46066  fourierdlem41  46177  fourierdlem48  46183  fourierdlem49  46184  fourierdlem74  46209  fourierdlem75  46210  salgencl  46361  salgenuni  46366  issalgend  46367  smfaddlem1  46792  funcoppc4  49087