Theorem simprrd 773

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fpwwe2lem3  10531  uzind  12571  latcl2  18344  clatlem  18410  dirge  18511  srgrz  20127  lmodvs1  20825  lmhmsca  20966  evlsvar  22026  uzsind  28330  mirbtwn  28637  dfcgra2  28809  3trlond  30155  3pthond  30157  3spthond  30159  ssdifidllem  33428  ssmxidllem  33445  ssmxidl  33446  axtgupdim2ALTV  34702  mvtinf  35620  rngoid  37962  rngoideu  37963  rngorn1eq  37994  rngomndo  37995  fzne2d  42093  mzpcl34  42848  icccncfext  46009  fourierdlem12  46241  fourierdlem34  46263  fourierdlem41  46270  fourierdlem48  46276  fourierdlem49  46277  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem89  46317  fourierdlem91  46319  fourierdlem92  46320  fourierdlem94  46322  fourierdlem113  46341  sssalgen  46457  issalgend  46460  smfaddlem1  46885  nelsubc2  49194  funcoppc4  49269