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  10748  uzind  12821  latcl2  18642  clatlem  18708  dirge  18809  srgrz  20466  lmodvs1  21198  lmhmsca  21338  ssdifidllem  21673  evlsvar  22437  uzsind  28824  mirbtwn  29163  dfcgra2  29371  3trlond  30807  3pthond  30809  3spthond  30811  edomediv  33936  ssmxidllem  34082  ssmxidl  34083  axtgupdim2ALTV  35380  mvtinf  36500  rngoid  39039  rngoideu  39040  rngorn1eq  39071  rngomndo  39072  fzne2d  43233  mzpcl34  43946  icccncfext  47112  fourierdlem12  47344  fourierdlem34  47366  fourierdlem41  47373  fourierdlem48  47379  fourierdlem49  47380  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem89  47420  fourierdlem91  47422  fourierdlem92  47423  fourierdlem94  47425  fourierdlem113  47444  sssalgen  47560  issalgend  47563  smfaddlem1  47988  nelsubc2  50398  funcoppc4  50475