MPE Home Metamath Proof Explorer < Wrap   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  idi Structured version   Visualization version   GIF version

Theorem idi 1
Description: (Note: This inference rule and the next one, a1ii 2, will normally never appear in a completed proof. They can be ignored if you are using this database to assist learning logic; please start with the statement wn 3 instead.)

This inference says "if 𝜑 is true then 𝜑 is true". This inference requires no axioms for its proof, and 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. You can remove this using the metamath-exe (Metamath program) Proof Assistant using the "MM-PA> MINIMIZEWITH *" command. This is the inference associated with id 22, hence its name. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
idi.1 𝜑
Ref Expression
idi 𝜑

Proof of Theorem idi
StepHypRef Expression
1 idi.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by:  madjusmdetlem2  30735  frege55lem2a  39576  fsovrfovd  39718  imo72b2lem0  39880  ssmapsn  40905  fprodcnlem  41312  limsupvaluz2  41451  dvmptfprod  41661  dvnprodlem1  41662  sge0f1o  42096  smfsupmpt  42521  smfinfmpt  42525  rngcifuestrc  43633
  Copyright terms: Public domain W3C validator