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  10592  uzind  12632  latcl2  18401  clatlem  18467  dirge  18568  srgrz  20122  lmodvs1  20802  lmhmsca  20943  evlsvar  22003  uzsind  28299  mirbtwn  28591  dfcgra2  28763  3trlond  30108  3pthond  30110  3spthond  30112  ssdifidllem  33433  ssmxidllem  33450  ssmxidl  33451  axtgupdim2ALTV  34665  mvtinf  35542  rngoid  37891  rngoideu  37892  rngorn1eq  37923  rngomndo  37924  fzne2d  41963  mzpcl34  42712  icccncfext  45878  fourierdlem12  46110  fourierdlem34  46132  fourierdlem41  46139  fourierdlem48  46145  fourierdlem49  46146  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem89  46186  fourierdlem91  46188  fourierdlem92  46189  fourierdlem94  46191  fourierdlem113  46210  sssalgen  46326  issalgend  46329  smfaddlem1  46754  nelsubc2  49048  funcoppc4  49123