|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > idiALT | Structured version Visualization version GIF version | ||
| Description: Placeholder for idi 1. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| idiALT.1 | ⊢ 𝜑 | 
| Ref | Expression | 
|---|---|
| idiALT | ⊢ 𝜑 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | idiALT.1 | 1 ⊢ 𝜑 | 
| Colors of variables: wff setvar class | 
| This theorem is referenced by: ax6e2nd 44583 trsspwALT2 44844 sspwtrALT 44847 suctrALT 44851 sstrALT2 44860 suctrALT3 44949 sspwimpALT 44950 ax6e2ndALT 44955 ax6e2ndeqALT 44956 isosctrlem1ALT 44959 iunconnlem2 44960 sineq0ALT 44962 | 
| Copyright terms: Public domain | W3C validator |