Theorem simprrd 771

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fpwwe2lem3  10390  uzind  12412  latcl2  18152  clatlem  18218  dirge  18319  srgrz  19760  lmodvs1  20149  lmhmsca  20290  evlsvar  21298  mirbtwn  27017  dfcgra2  27189  3trlond  28533  3pthond  28535  3spthond  28537  ssmxidllem  31637  ssmxidl  31638  axtgupdim2ALTV  32644  mvtinf  33513  rngoid  36056  rngoideu  36057  rngorn1eq  36088  rngomndo  36089  fzne2d  39986  mzpcl34  40550  icccncfext  43399  fourierdlem12  43631  fourierdlem34  43653  fourierdlem41  43660  fourierdlem48  43666  fourierdlem49  43667  fourierdlem74  43692  fourierdlem75  43693  fourierdlem76  43694  fourierdlem89  43707  fourierdlem91  43709  fourierdlem92  43710  fourierdlem94  43712  fourierdlem113  43731  sssalgen  43845  issalgend  43848  smfaddlem1  44266