Theorem simprrd 779

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fpwwe2lem3  10554  uzind  12619  latcl2  18400  clatlem  18466  dirge  18567  srgrz  20186  lmodvs1  20887  lmhmsca  21027  evlsvar  22078  uzsind  28422  mirbtwn  28751  dfcgra2  28923  3trlond  30268  3pthond  30270  3spthond  30272  ssdifidllem  33546  ssmxidllem  33563  ssmxidl  33564  axtgupdim2ALTV  34859  mvtinf  35790  rngoid  38276  rngoideu  38277  rngorn1eq  38308  rngomndo  38309  fzne2d  42472  mzpcl34  43187  icccncfext  46337  fourierdlem12  46569  fourierdlem34  46591  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem89  46645  fourierdlem91  46647  fourierdlem92  46648  fourierdlem94  46650  fourierdlem113  46669  sssalgen  46785  issalgend  46788  smfaddlem1  47213  nelsubc2  49566  funcoppc4  49641