Theorem simprrd 783

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fpwwe2lem3  10588  uzind  12662  latcl2  18451  clatlem  18517  dirge  18618  srgrz  20236  lmodvs1  20937  lmhmsca  21077  evlsvar  22128  uzsind  28475  mirbtwn  28804  dfcgra2  28976  3trlond  30321  3pthond  30323  3spthond  30325  ssdifidllem  33604  ssmxidllem  33622  ssmxidl  33623  axtgupdim2ALTV  34926  mvtinf  35869  rngoid  38365  rngoideu  38366  rngorn1eq  38397  rngomndo  38398  fzne2d  42561  mzpcl34  43276  icccncfext  46425  fourierdlem12  46657  fourierdlem34  46679  fourierdlem41  46686  fourierdlem48  46692  fourierdlem49  46693  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem89  46733  fourierdlem91  46735  fourierdlem92  46736  fourierdlem94  46738  fourierdlem113  46757  sssalgen  46873  issalgend  46876  smfaddlem1  47301  nelsubc2  49654  funcoppc4  49729