Theorem simprrd 793

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  fpwwe2lem3  9334  uzind  11345  latcl2  16871  clatlem  16934  dirge  17060  srgrz  18349  lmodvs1  18714  lmhmsca  18851  evlsvar  19344  mirbtwn  25353  dfcgra2  25521  trlonistrl  26073  pthonispth  26108  spthonisspth  26116  numclwwlk2lem1  26629  axtgupdim2OLD  29999  mvtinf  30706  rngoid  32871  rngoideu  32872  rngorn1eq  32903  rngomndo  32904  mzpcl34  36312  icccncfext  38773  fourierdlem12  39012  fourierdlem34  39034  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  fourierdlem94  39093  fourierdlem113  39112  sssalgen  39229  issalgend  39232  smfaddlem1  39649  3trlond  41340  3pthond  41342  3spthond  41344