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  10547  uzind  12612  latcl2  18393  clatlem  18459  dirge  18560  srgrz  20179  lmodvs1  20876  lmhmsca  21017  evlsvar  22083  uzsind  28411  mirbtwn  28740  dfcgra2  28912  3trlond  30258  3pthond  30260  3spthond  30262  ssdifidllem  33531  ssmxidllem  33548  ssmxidl  33549  axtgupdim2ALTV  34828  mvtinf  35753  rngoid  38237  rngoideu  38238  rngorn1eq  38269  rngomndo  38270  fzne2d  42433  mzpcl34  43177  icccncfext  46333  fourierdlem12  46565  fourierdlem34  46587  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem89  46641  fourierdlem91  46643  fourierdlem92  46644  fourierdlem94  46646  fourierdlem113  46665  sssalgen  46781  issalgend  46784  smfaddlem1  47209  nelsubc2  49556  funcoppc4  49631