MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprrd Structured version   Visualization version   Unicode version

Theorem simprrd 775
Description: Deduction form of simprr 774, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
simprrd.1  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
Assertion
Ref Expression
simprrd  |-  ( ph  ->  th )

Proof of Theorem simprrd
StepHypRef Expression
1 simprrd.1 . . 3  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
21simprd 470 . 2  |-  ( ph  ->  ( ch  /\  th ) )
32simprd 470 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  fpwwe2lem3  9076  uzind  11050  latcl2  16372  clatlem  16435  dirge  16561  srgrz  17837  lmodvs1  18197  lmhmsca  18331  evlsvar  18823  mirbtwn  24782  dfcgra2  24950  trlonistrl  25352  pthonispth  25387  spthonisspth  25395  numclwwlk2lem1  25909  rngoid  26192  rngoideu  26193  rngorn1eq  26229  rngomndo  26230  axtgupdim2OLD  29557  mvtinf  30265  mzpcl34  35644  icccncfext  37862  fourierdlem12  38093  fourierdlem34  38116  fourierdlem41  38123  fourierdlem48  38130  fourierdlem49  38131  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem89  38171  fourierdlem91  38173  fourierdlem92  38174  fourierdlem94  38176  fourierdlem113  38195  sssalgen  38306  issalgend  38309  3trlond  40087  3pthond  40089  3spthond  40091
  Copyright terms: Public domain W3C validator