Theorem simprrd 785

Description: Deduction form of simprr 784, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
simprrd.1	⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simprrd	⊢ (𝜑 → 𝜃)

Proof of Theorem simprrd

Step	Hyp	Ref	Expression
1		simprrd.1	. . 3 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
2	1	simprd 500	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
3	2	simprd 500	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fpwwe2lem3  10619  uzind  12689  latcl2  18493  clatlem  18559  dirge  18660  srgrz  20290  lmodvs1  20992  lmhmsca  21132  ssdifidllem  21465  evlsvar  22227  uzsind  28579  mirbtwn  28916  dfcgra2  29122  3trlond  30505  3pthond  30507  3spthond  30509  ssmxidllem  33737  ssmxidl  33738  axtgupdim2ALTV  35036  mvtinf  36028  rngoid  38534  rngoideu  38535  rngorn1eq  38566  rngomndo  38567  fzne2d  42728  mzpcl34  43445  icccncfext  46584  fourierdlem12  46816  fourierdlem34  46838  fourierdlem41  46845  fourierdlem48  46851  fourierdlem49  46852  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem89  46892  fourierdlem91  46894  fourierdlem92  46895  fourierdlem94  46897  fourierdlem113  46916  sssalgen  47032  issalgend  47035  smfaddlem1  47460  nelsubc2  49830  funcoppc4  49905