Theorem simprrd 814

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  fpwwe2lem3  9647  uzind  11661  latcl2  17249  clatlem  17312  dirge  17438  srgrz  18726  lmodvs1  19093  lmhmsca  19232  evlsvar  19725  mirbtwn  25752  dfcgra2  25920  3trlond  27325  3pthond  27327  3spthond  27329  axtgupdim2OLD  31055  mvtinf  31759  rngoid  34014  rngoideu  34015  rngorn1eq  34046  rngomndo  34047  mzpcl34  37796  icccncfext  40603  fourierdlem12  40839  fourierdlem34  40861  fourierdlem41  40868  fourierdlem48  40874  fourierdlem49  40875  fourierdlem74  40900  fourierdlem75  40901  fourierdlem76  40902  fourierdlem89  40915  fourierdlem91  40917  fourierdlem92  40918  fourierdlem94  40920  fourierdlem113  40939  sssalgen  41056  issalgend  41059  smfaddlem1  41477