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

This theorem is referenced by:  fpwwe2lem3  10044  uzind  12062  latcl2  17650  clatlem  17713  dirge  17839  srgrz  19269  lmodvs1  19655  lmhmsca  19795  evlsvar  20762  mirbtwn  26452  dfcgra2  26624  3trlond  27958  3pthond  27960  3spthond  27962  ssmxidllem  31049  ssmxidl  31050  axtgupdim2ALTV  32049  mvtinf  32915  rngoid  35340  rngoideu  35341  rngorn1eq  35372  rngomndo  35373  fzne2d  39268  mzpcl34  39672  icccncfext  42529  fourierdlem12  42761  fourierdlem34  42783  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem89  42837  fourierdlem91  42839  fourierdlem92  42840  fourierdlem94  42842  fourierdlem113  42861  sssalgen  42975  issalgend  42978  smfaddlem1  43396