Theorem simprrd 771

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  fpwwe2lem3  10389  uzind  12412  latcl2  18154  clatlem  18220  dirge  18321  srgrz  19762  lmodvs1  20151  lmhmsca  20292  evlsvar  21300  mirbtwn  27019  dfcgra2  27191  3trlond  28537  3pthond  28539  3spthond  28541  ssmxidllem  31641  ssmxidl  31642  axtgupdim2ALTV  32648  mvtinf  33517  rngoid  36060  rngoideu  36061  rngorn1eq  36092  rngomndo  36093  fzne2d  39989  mzpcl34  40553  icccncfext  43428  fourierdlem12  43660  fourierdlem34  43682  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem89  43736  fourierdlem91  43738  fourierdlem92  43739  fourierdlem94  43741  fourierdlem113  43760  sssalgen  43874  issalgend  43877  smfaddlem1  44298