Theorem simprrd 764

Description: Deduction form of simprr 763, 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 491	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
3	2	simprd 491	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  fpwwe2lem3  9790  uzind  11821  latcl2  17434  clatlem  17497  dirge  17623  srgrz  18913  lmodvs1  19283  lmhmsca  19425  evlsvar  19919  mirbtwn  26009  dfcgra2  26178  3trlond  27576  3pthond  27578  3spthond  27580  axtgupdim2OLD  31348  mvtinf  32051  rngoid  34325  rngoideu  34326  rngorn1eq  34357  rngomndo  34358  mzpcl34  38254  icccncfext  41028  fourierdlem12  41263  fourierdlem34  41285  fourierdlem41  41292  fourierdlem48  41298  fourierdlem49  41299  fourierdlem74  41324  fourierdlem75  41325  fourierdlem76  41326  fourierdlem89  41339  fourierdlem91  41341  fourierdlem92  41342  fourierdlem94  41344  fourierdlem113  41363  sssalgen  41477  issalgend  41480  smfaddlem1  41898