Theorem simprrd 770

Description: Deduction form of simprr 769, 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 206  df-an 396

This theorem is referenced by:  fpwwe2lem3  10320  uzind  12342  latcl2  18069  clatlem  18135  dirge  18236  srgrz  19677  lmodvs1  20066  lmhmsca  20207  evlsvar  21210  mirbtwn  26923  dfcgra2  27095  3trlond  28438  3pthond  28440  3spthond  28442  ssmxidllem  31543  ssmxidl  31544  axtgupdim2ALTV  32548  mvtinf  33417  rngoid  35987  rngoideu  35988  rngorn1eq  36019  rngomndo  36020  fzne2d  39917  mzpcl34  40469  icccncfext  43318  fourierdlem12  43550  fourierdlem34  43572  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem89  43626  fourierdlem91  43628  fourierdlem92  43629  fourierdlem94  43631  fourierdlem113  43650  sssalgen  43764  issalgend  43767  smfaddlem1  44185