Theorem simprrd 774

Description: Deduction form of simprr 773, 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  10556  uzind  12621  latcl2  18402  clatlem  18468  dirge  18569  srgrz  20188  lmodvs1  20885  lmhmsca  21025  evlsvar  22073  uzsind  28397  mirbtwn  28726  dfcgra2  28898  3trlond  30243  3pthond  30245  3spthond  30247  ssdifidllem  33516  ssmxidllem  33533  ssmxidl  33534  axtgupdim2ALTV  34812  mvtinf  35737  rngoid  38223  rngoideu  38224  rngorn1eq  38255  rngomndo  38256  fzne2d  42419  mzpcl34  43163  icccncfext  46315  fourierdlem12  46547  fourierdlem34  46569  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem89  46623  fourierdlem91  46625  fourierdlem92  46626  fourierdlem94  46628  fourierdlem113  46647  sssalgen  46763  issalgend  46766  smfaddlem1  47191  nelsubc2  49544  funcoppc4  49619