Theorem simprrd 770

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  fpwwe2lem3  10630  uzind  12658  latcl2  18393  clatlem  18459  dirge  18560  srgrz  20101  lmodvs1  20644  lmhmsca  20785  evlsvar  21872  mirbtwn  28176  dfcgra2  28348  3trlond  29693  3pthond  29695  3spthond  29697  ssmxidllem  32863  ssmxidl  32864  axtgupdim2ALTV  33978  mvtinf  34844  rngoid  37073  rngoideu  37074  rngorn1eq  37105  rngomndo  37106  fzne2d  41152  mzpcl34  41771  icccncfext  44901  fourierdlem12  45133  fourierdlem34  45155  fourierdlem41  45162  fourierdlem48  45168  fourierdlem49  45169  fourierdlem74  45194  fourierdlem75  45195  fourierdlem76  45196  fourierdlem89  45209  fourierdlem91  45211  fourierdlem92  45212  fourierdlem94  45214  fourierdlem113  45233  sssalgen  45349  issalgend  45352  smfaddlem1  45777