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  10521  uzind  12562  latcl2  18339  clatlem  18405  dirge  18506  srgrz  20123  lmodvs1  20821  lmhmsca  20962  evlsvar  22023  uzsind  28327  mirbtwn  28634  dfcgra2  28806  3trlond  30148  3pthond  30150  3spthond  30152  ssdifidllem  33416  ssmxidllem  33433  ssmxidl  33434  axtgupdim2ALTV  34676  mvtinf  35587  rngoid  37941  rngoideu  37942  rngorn1eq  37973  rngomndo  37974  fzne2d  42012  mzpcl34  42763  icccncfext  45924  fourierdlem12  46156  fourierdlem34  46178  fourierdlem41  46185  fourierdlem48  46191  fourierdlem49  46192  fourierdlem74  46217  fourierdlem75  46218  fourierdlem76  46219  fourierdlem89  46232  fourierdlem91  46234  fourierdlem92  46235  fourierdlem94  46237  fourierdlem113  46256  sssalgen  46372  issalgend  46375  smfaddlem1  46800  nelsubc2  49100  funcoppc4  49175