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  27803  mulc1cncfg  27824  climsuse  27837  stoweidlem3  27855  stoweidlem11  27863  stoweidlem14  27866  stoweidlem25  27877  stoweidlem26  27878  stoweidlem29  27881  stoweidlem34  27886  stoweidlem36  27888  stoweidlem38  27890  stoweidlem42  27894  stoweidlem43  27895  stoweidlem44  27896  stoweidlem48  27900  stoweidlem52  27904  stoweidlem56  27908  stoweidlem59  27911  stoweid  27915  wallispilem5  27921  stirlinglem13  27938  onfrALTlem2  28610  a9e2nd  28623  e233  28854  trsspwALT2  28909  sspwtrALT  28912  sstrALT2  28927  suctrALT3  29016  sspwimpALT  29017  notnot2ALT2  29019  suctrALT4  29020  sspwimpALT2  29021  a9e2ndALT  29023  a9e2ndeqALT  29024
  Copyright terms: Public domain W3C validator