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

Theorem idi 2
Description: Inference form of id 19. This inference rule, which requires no axioms for its proof, is useful as a copy-paste mechanism during proof development in mmj2. It is normally not referenced in the final version of a proof, since it is always redundant and can be removed using the 'minimize *' command in the metamath program's Proof Assistant. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
idi.1  |-  ph
Assertion
Ref Expression
idi  |-  ph

Proof of Theorem idi
StepHypRef Expression
1 idi.1 1  |-  ph
Colors of variables: wff set class
This theorem is referenced by:  dvrec  19320  fnchoice  27802  mulc1cncfg  27823  climsuse  27836  stoweidlem3  27854  stoweidlem11  27862  stoweidlem14  27865  stoweidlem25  27876  stoweidlem26  27877  stoweidlem29  27880  stoweidlem34  27885  stoweidlem36  27887  stoweidlem38  27889  stoweidlem42  27893  stoweidlem43  27894  stoweidlem44  27895  stoweidlem48  27899  stoweidlem52  27903  stoweidlem56  27907  stoweidlem59  27910  stoweid  27914  wallispilem5  27920  stirlinglem13  27937  onfrALTlem2  28609  a9e2nd  28622  e233  28853  trsspwALT2  28908  sspwtrALT  28911  sstrALT2  28926  suctrALT3  29015  sspwimpALT  29016  notnot2ALT2  29018  suctrALT4  29019  sspwimpALT2  29020  a9e2ndALT  29022  a9e2ndeqALT  29023
  Copyright terms: Public domain W3C validator