Metamath Proof Explorer

Table of Contents - 20.38.7. Theorems proved using Virtual Deduction with mmj2 assistance

1. simplbi2VD
2. 3ornot23VD
3. orbi1rVD
4. bitr3VD
5. 3orbi123VD
6. sbc3orgVD
7. 19.21a3con13vVD
8. exbirVD
9. exbiriVD
10. rspsbc2VD
11. 3impexpVD
12. 3impexpbicomVD
13. 3impexpbicomiVD
14. sbcoreleleqVD
15. hbra2VD
16. tratrbVD
17. al2imVD
18. syl5impVD
19. idiVD
20. ancomstVD
21. ssralv2VD
22. ordelordALTVD
23. equncomVD
24. equncomiVD
25. sucidALTVD
26. sucidALT
27. sucidVD
28. imbi12VD
29. imbi13VD
30. sbcim2gVD
31. sbcbiVD
32. trsbcVD
33. truniALTVD
34. ee33VD
35. trintALTVD
36. trintALT
37. undif3VD
38. sbcssgVD
39. csbingVD
40. onfrALTlem5VD
41. onfrALTlem4VD
42. onfrALTlem3VD
43. simplbi2comtVD
44. onfrALTlem2VD
45. onfrALTlem1VD
46. onfrALTVD
47. csbeq2gVD
48. csbsngVD
49. csbxpgVD
50. csbresgVD
51. csbrngVD
52. csbima12gALTVD
53. csbunigVD
54. csbfv12gALTVD
55. con5VD
56. relopabVD
57. 19.41rgVD
58. 2pm13.193VD
59. hbimpgVD
60. hbalgVD
61. hbexgVD
62. ax6e2eqVD
63. ax6e2ndVD
64. ax6e2ndeqVD
65. 2sb5ndVD
66. 2uasbanhVD
67. e2ebindVD