Theorem simprrd 797

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  fpwwe2lem3  9455  uzind  11469  latcl2  17048  clatlem  17111  dirge  17237  srgrz  18526  lmodvs1  18891  lmhmsca  19030  evlsvar  19523  mirbtwn  25553  dfcgra2  25721  3trlond  27033  3pthond  27035  3spthond  27037  axtgupdim2OLD  30746  mvtinf  31452  rngoid  33701  rngoideu  33702  rngorn1eq  33733  rngomndo  33734  mzpcl34  37294  icccncfext  40100  fourierdlem12  40336  fourierdlem34  40358  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem89  40412  fourierdlem91  40414  fourierdlem92  40415  fourierdlem94  40417  fourierdlem113  40436  sssalgen  40553  issalgend  40556  smfaddlem1  40971