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  10636  uzind  12706  latcl2  18517  clatlem  18583  dirge  18684  srgrz  20320  lmodvs1  21048  lmhmsca  21188  ssdifidllem  21521  evlsvar  22283  uzsind  28635  mirbtwn  28972  dfcgra2  29178  3trlond  30561  3pthond  30563  3spthond  30565  ssmxidllem  33787  ssmxidl  33788  axtgupdim2ALTV  35087  mvtinf  36068  rngoid  38594  rngoideu  38595  rngorn1eq  38626  rngomndo  38627  fzne2d  42788  mzpcl34  43503  icccncfext  46642  fourierdlem12  46874  fourierdlem34  46896  fourierdlem41  46903  fourierdlem48  46909  fourierdlem49  46910  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem89  46950  fourierdlem91  46952  fourierdlem92  46953  fourierdlem94  46955  fourierdlem113  46974  sssalgen  47090  issalgend  47093  smfaddlem1  47518  nelsubc2  49888  funcoppc4  49963