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 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  10630  uzind  12658  latcl2  18401  clatlem  18467  dirge  18568  srgrz  20112  lmodvs1  20736  lmhmsca  20878  evlsvar  21995  mirbtwn  28417  dfcgra2  28589  3trlond  29935  3pthond  29937  3spthond  29939  ssmxidllem  33095  ssmxidl  33096  axtgupdim2ALTV  34209  mvtinf  35074  rngoid  37283  rngoideu  37284  rngorn1eq  37315  rngomndo  37316  fzne2d  41362  mzpcl34  42052  icccncfext  45180  fourierdlem12  45412  fourierdlem34  45434  fourierdlem41  45441  fourierdlem48  45447  fourierdlem49  45448  fourierdlem74  45473  fourierdlem75  45474  fourierdlem76  45475  fourierdlem89  45488  fourierdlem91  45490  fourierdlem92  45491  fourierdlem94  45493  fourierdlem113  45512  sssalgen  45628  issalgend  45631  smfaddlem1  46056