Theorem simprrd 786

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fpwwe2lem3  10721  uzind  12794  latcl2  18615  clatlem  18681  dirge  18782  srgrz  20438  lmodvs1  21170  lmhmsca  21310  ssdifidllem  21645  evlsvar  22409  uzsind  28796  mirbtwn  29135  dfcgra2  29343  3trlond  30779  3pthond  30781  3spthond  30783  ssmxidllem  34044  ssmxidl  34045  axtgupdim2ALTV  35343  mvtinf  36406  rngoid  38929  rngoideu  38930  rngorn1eq  38961  rngomndo  38962  fzne2d  43123  mzpcl34  43835  icccncfext  46990  fourierdlem12  47222  fourierdlem34  47244  fourierdlem41  47251  fourierdlem48  47257  fourierdlem49  47258  fourierdlem74  47283  fourierdlem75  47284  fourierdlem76  47285  fourierdlem89  47298  fourierdlem91  47300  fourierdlem92  47301  fourierdlem94  47303  fourierdlem113  47322  sssalgen  47438  issalgend  47441  smfaddlem1  47866  nelsubc2  50276  funcoppc4  50353