Theorem simprrd 772

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fpwwe2lem3  10057  uzind  12077  latcl2  17660  clatlem  17723  dirge  17849  srgrz  19278  lmodvs1  19664  lmhmsca  19804  evlsvar  20305  mirbtwn  26446  dfcgra2  26618  3trlond  27954  3pthond  27956  3spthond  27958  ssmxidllem  30980  ssmxidl  30981  axtgupdim2ALTV  31941  mvtinf  32804  rngoid  35182  rngoideu  35183  rngorn1eq  35214  rngomndo  35215  mzpcl34  39335  icccncfext  42177  fourierdlem12  42411  fourierdlem34  42433  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem89  42487  fourierdlem91  42489  fourierdlem92  42490  fourierdlem94  42492  fourierdlem113  42511  sssalgen  42625  issalgend  42628  smfaddlem1  43046