Theorem simprrd 780

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

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  fpwwe2lem3  10551  uzind  12616  latcl2  18397  clatlem  18463  dirge  18564  srgrz  20183  lmodvs1  20884  lmhmsca  21024  evlsvar  22075  uzsind  28419  mirbtwn  28748  dfcgra2  28920  3trlond  30265  3pthond  30267  3spthond  30269  ssdifidllem  33543  ssmxidllem  33560  ssmxidl  33561  axtgupdim2ALTV  34864  mvtinf  35798  rngoid  38284  rngoideu  38285  rngorn1eq  38316  rngomndo  38317  fzne2d  42480  mzpcl34  43195  icccncfext  46344  fourierdlem12  46576  fourierdlem34  46598  fourierdlem41  46605  fourierdlem48  46611  fourierdlem49  46612  fourierdlem74  46637  fourierdlem75  46638  fourierdlem76  46639  fourierdlem89  46652  fourierdlem91  46654  fourierdlem92  46655  fourierdlem94  46657  fourierdlem113  46676  sssalgen  46792  issalgend  46795  smfaddlem1  47220  nelsubc2  49573  funcoppc4  49648