Theorem simprrd 786

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fpwwe2lem3  10646  uzind  12717  latcl2  18530  clatlem  18596  dirge  18697  srgrz  20352  lmodvs1  21080  lmhmsca  21220  ssdifidllem  21553  evlsvar  22317  uzsind  28678  mirbtwn  29017  dfcgra2  29225  3trlond  30661  3pthond  30663  3spthond  30665  ssmxidllem  33884  ssmxidl  33885  axtgupdim2ALTV  35184  mvtinf  36142  rngoid  38660  rngoideu  38661  rngorn1eq  38692  rngomndo  38693  fzne2d  42854  mzpcl34  43584  icccncfext  46723  fourierdlem12  46955  fourierdlem34  46977  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem89  47031  fourierdlem91  47033  fourierdlem92  47034  fourierdlem94  47036  fourierdlem113  47055  sssalgen  47171  issalgend  47174  smfaddlem1  47599  nelsubc2  50003  funcoppc4  50078