Theorem simprrd 774

Description: Deduction form of simprr 773, 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  10671  uzind  12708  latcl2  18494  clatlem  18560  dirge  18661  srgrz  20225  lmodvs1  20905  lmhmsca  21047  evlsvar  22132  uzsind  28406  mirbtwn  28681  dfcgra2  28853  3trlond  30202  3pthond  30204  3spthond  30206  ssdifidllem  33464  ssmxidllem  33481  ssmxidl  33482  axtgupdim2ALTV  34662  mvtinf  35540  rngoid  37889  rngoideu  37890  rngorn1eq  37921  rngomndo  37922  fzne2d  41962  mzpcl34  42719  icccncfext  45843  fourierdlem12  46075  fourierdlem34  46097  fourierdlem41  46104  fourierdlem48  46110  fourierdlem49  46111  fourierdlem74  46136  fourierdlem75  46137  fourierdlem76  46138  fourierdlem89  46151  fourierdlem91  46153  fourierdlem92  46154  fourierdlem94  46156  fourierdlem113  46175  sssalgen  46291  issalgend  46294  smfaddlem1  46719