Theorem simprrd 774

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

This theorem is referenced by:  fpwwe2lem3  10556  uzind  12596  latcl2  18371  clatlem  18437  dirge  18538  srgrz  20154  lmodvs1  20853  lmhmsca  20994  evlsvar  22062  uzsind  28413  mirbtwn  28742  dfcgra2  28914  3trlond  30260  3pthond  30262  3spthond  30264  ssdifidllem  33548  ssmxidllem  33565  ssmxidl  33566  axtgupdim2ALTV  34845  mvtinf  35768  rngoid  38147  rngoideu  38148  rngorn1eq  38179  rngomndo  38180  fzne2d  42344  mzpcl34  43082  icccncfext  46239  fourierdlem12  46471  fourierdlem34  46493  fourierdlem41  46500  fourierdlem48  46506  fourierdlem49  46507  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem89  46547  fourierdlem91  46549  fourierdlem92  46550  fourierdlem94  46552  fourierdlem113  46571  sssalgen  46687  issalgend  46690  smfaddlem1  47115  nelsubc2  49422  funcoppc4  49497