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  10586  uzind  12626  latcl2  18395  clatlem  18461  dirge  18562  srgrz  20116  lmodvs1  20796  lmhmsca  20937  evlsvar  21997  uzsind  28293  mirbtwn  28585  dfcgra2  28757  3trlond  30102  3pthond  30104  3spthond  30106  ssdifidllem  33427  ssmxidllem  33444  ssmxidl  33445  axtgupdim2ALTV  34659  mvtinf  35542  rngoid  37896  rngoideu  37897  rngorn1eq  37928  rngomndo  37929  fzne2d  41968  mzpcl34  42719  icccncfext  45885  fourierdlem12  46117  fourierdlem34  46139  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem89  46193  fourierdlem91  46195  fourierdlem92  46196  fourierdlem94  46198  fourierdlem113  46217  sssalgen  46333  issalgend  46336  smfaddlem1  46761  nelsubc2  49055  funcoppc4  49130