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  10674  uzind  12712  latcl2  18482  clatlem  18548  dirge  18649  srgrz  20205  lmodvs1  20889  lmhmsca  21030  evlsvar  22115  uzsind  28392  mirbtwn  28667  dfcgra2  28839  3trlond  30193  3pthond  30195  3spthond  30197  ssdifidllem  33485  ssmxidllem  33502  ssmxidl  33503  axtgupdim2ALTV  34684  mvtinf  35561  rngoid  37910  rngoideu  37911  rngorn1eq  37942  rngomndo  37943  fzne2d  41982  mzpcl34  42747  icccncfext  45907  fourierdlem12  46139  fourierdlem34  46161  fourierdlem41  46168  fourierdlem48  46174  fourierdlem49  46175  fourierdlem74  46200  fourierdlem75  46201  fourierdlem76  46202  fourierdlem89  46215  fourierdlem91  46217  fourierdlem92  46218  fourierdlem94  46220  fourierdlem113  46239  sssalgen  46355  issalgend  46358  smfaddlem1  46783