Metamath Proof Explorer

Table of Contents - 20.38.11. Theorems with a proof in conventional notation derived from a VD proof

Theorems with a proof in conventional notation automatically derived by completeusersproof.c from a Virtual Deduction User's Proof.

1. notnotrALT2
2. sspwimpALT2
3. e2ebindALT
4. ax6e2ndALT
5. ax6e2ndeqALT
6. 2sb5ndALT
7. chordthmALT
8. isosctrlem1ALT
9. iunconnlem2
10. iunconnALT
11. sineq0ALT