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  10699  uzind  12772  latcl2  18590  clatlem  18656  dirge  18757  srgrz  20413  lmodvs1  21145  lmhmsca  21285  ssdifidllem  21620  evlsvar  22384  uzsind  28773  mirbtwn  29112  dfcgra2  29320  3trlond  30756  3pthond  30758  3spthond  30760  ssmxidllem  33980  ssmxidl  33981  axtgupdim2ALTV  35280  mvtinf  36289  rngoid  38804  rngoideu  38805  rngorn1eq  38836  rngomndo  38837  fzne2d  42998  mzpcl34  43695  icccncfext  46841  fourierdlem12  47073  fourierdlem34  47095  fourierdlem41  47102  fourierdlem48  47108  fourierdlem49  47109  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem89  47149  fourierdlem91  47151  fourierdlem92  47152  fourierdlem94  47154  fourierdlem113  47173  sssalgen  47289  issalgend  47292  smfaddlem1  47717  nelsubc2  50121  funcoppc4  50196