Theorem simprrd 773

Description: Deduction form of simprr 772, 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  10702  uzind  12735  latcl2  18506  clatlem  18572  dirge  18673  srgrz  20234  lmodvs1  20910  lmhmsca  21052  evlsvar  22137  uzsind  28409  mirbtwn  28684  dfcgra2  28856  3trlond  30205  3pthond  30207  3spthond  30209  ssdifidllem  33449  ssmxidllem  33466  ssmxidl  33467  axtgupdim2ALTV  34645  mvtinf  35523  rngoid  37862  rngoideu  37863  rngorn1eq  37894  rngomndo  37895  fzne2d  41937  mzpcl34  42687  icccncfext  45808  fourierdlem12  46040  fourierdlem34  46062  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem89  46116  fourierdlem91  46118  fourierdlem92  46119  fourierdlem94  46121  fourierdlem113  46140  sssalgen  46256  issalgend  46259  smfaddlem1  46684