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  10544  uzind  12584  latcl2  18359  clatlem  18425  dirge  18526  srgrz  20142  lmodvs1  20841  lmhmsca  20982  evlsvar  22050  uzsind  28401  mirbtwn  28730  dfcgra2  28902  3trlond  30248  3pthond  30250  3spthond  30252  ssdifidllem  33537  ssmxidllem  33554  ssmxidl  33555  axtgupdim2ALTV  34825  mvtinf  35749  rngoid  38099  rngoideu  38100  rngorn1eq  38131  rngomndo  38132  fzne2d  42230  mzpcl34  42969  icccncfext  46127  fourierdlem12  46359  fourierdlem34  46381  fourierdlem41  46388  fourierdlem48  46394  fourierdlem49  46395  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem89  46435  fourierdlem91  46437  fourierdlem92  46438  fourierdlem94  46440  fourierdlem113  46459  sssalgen  46575  issalgend  46578  smfaddlem1  47003  nelsubc2  49310  funcoppc4  49385