Theorem simprrd 773

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fpwwe2lem3  10652  uzind  12690  latcl2  18451  clatlem  18517  dirge  18618  srgrz  20172  lmodvs1  20852  lmhmsca  20993  evlsvar  22053  uzsind  28350  mirbtwn  28642  dfcgra2  28814  3trlond  30159  3pthond  30161  3spthond  30163  ssdifidllem  33476  ssmxidllem  33493  ssmxidl  33494  axtgupdim2ALTV  34705  mvtinf  35582  rngoid  37931  rngoideu  37932  rngorn1eq  37963  rngomndo  37964  fzne2d  41998  mzpcl34  42721  icccncfext  45883  fourierdlem12  46115  fourierdlem34  46137  fourierdlem41  46144  fourierdlem48  46150  fourierdlem49  46151  fourierdlem74  46176  fourierdlem75  46177  fourierdlem76  46178  fourierdlem89  46191  fourierdlem91  46193  fourierdlem92  46194  fourierdlem94  46196  fourierdlem113  46215  sssalgen  46331  issalgend  46334  smfaddlem1  46759  nelsubc2  49003  funcoppc4  49054