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  19304  fnchoice  27700  mulc1cncfg  27721  climsuse  27734  stoweidlem3  27752  stoweidlem11  27760  stoweidlem14  27763  stoweidlem25  27774  stoweidlem26  27775  stoweidlem29  27778  stoweidlem34  27783  stoweidlem36  27785  stoweidlem38  27787  stoweidlem42  27791  stoweidlem43  27792  stoweidlem44  27793  stoweidlem48  27797  stoweidlem52  27801  stoweidlem56  27805  stoweidlem59  27808  stoweid  27812  wallispilem5  27818  stirlinglem13  27835  onfrALTlem2  28311  a9e2nd  28324  e233  28540  trsspwALT2  28593  sspwtrALT  28596  sstrALT2  28611  suctrALT3  28700  sspwimpALT  28701  notnot2ALT2  28703  suctrALT4  28704  sspwimpALT2  28705  a9e2ndALT  28707  a9e2ndeqALT  28708
  Copyright terms: Public domain W3C validator