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  10606  uzind  12679  latcl2  18482  clatlem  18548  dirge  18649  srgrz  20280  lmodvs1  20980  lmhmsca  21120  ssdifidllem  21444  evlsvar  22206  uzsind  28556  mirbtwn  28889  dfcgra2  29082  3trlond  30433  3pthond  30435  3spthond  30437  ssmxidllem  33673  ssmxidl  33674  axtgupdim2ALTV  34972  mvtinf  35918  rngoid  38413  rngoideu  38414  rngorn1eq  38445  rngomndo  38446  fzne2d  42609  mzpcl34  43324  icccncfext  46459  fourierdlem12  46691  fourierdlem34  46713  fourierdlem41  46720  fourierdlem48  46726  fourierdlem49  46727  fourierdlem74  46752  fourierdlem75  46753  fourierdlem76  46754  fourierdlem89  46767  fourierdlem91  46769  fourierdlem92  46770  fourierdlem94  46772  fourierdlem113  46791  sssalgen  46907  issalgend  46910  smfaddlem1  47335  nelsubc2  49698  funcoppc4  49773