Metamath Proof Explorer

Table of Contents - 20.38.5. Virtual Deduction Theorems

  1. df-vd1
  2. in1
  3. iin1
  4. dfvd1ir
  5. idn1
  6. dfvd1imp
  7. dfvd1impr
  8. wvd2
  9. df-vd2
  10. dfvd2
  11. wvhc2
  12. df-vhc2
  13. dfvd2an
  14. dfvd2ani
  15. dfvd2anir
  16. dfvd2i
  17. dfvd2ir
  18. wvd3
  19. wvhc3
  20. df-vhc3
  21. df-vd3
  22. dfvd3
  23. dfvd3i
  24. dfvd3ir
  25. dfvd3an
  26. dfvd3ani
  27. dfvd3anir
  28. vd01
  29. vd02
  30. vd03
  31. vd12
  32. vd13
  33. vd23
  34. dfvd2imp
  35. dfvd2impr
  36. in2
  37. int2
  38. iin2
  39. in2an
  40. in3
  41. iin3
  42. in3an
  43. int3
  44. idn2
  45. iden2
  46. idn3
  47. gen11
  48. gen11nv
  49. gen12
  50. gen21
  51. gen21nv
  52. gen31
  53. gen22
  54. ggen22
  55. exinst
  56. exinst01
  57. exinst11
  58. e1a
  59. el1
  60. e1bi
  61. e1bir
  62. e2
  63. e2bi
  64. e2bir
  65. ee223
  66. e223
  67. e222
  68. e220
  69. ee220
  70. e202
  71. ee202
  72. e022
  73. ee022
  74. e002
  75. ee002
  76. e020
  77. ee020
  78. e200
  79. ee200
  80. e221
  81. ee221
  82. e212
  83. ee212
  84. e122
  85. e112
  86. ee112
  87. e121
  88. e211
  89. ee211
  90. e210
  91. ee210
  92. e201
  93. ee201
  94. e120
  95. ee120
  96. e021
  97. ee021
  98. e012
  99. ee012
  100. e102
  101. ee102
  102. e22
  103. e22an
  104. ee22an
  105. e111
  106. e1111
  107. e110
  108. ee110
  109. e101
  110. ee101
  111. e011
  112. ee011
  113. e100
  114. ee100
  115. e010
  116. ee010
  117. e001
  118. ee001
  119. e11
  120. e11an
  121. ee11an
  122. e01
  123. e01an
  124. ee01an
  125. e10
  126. e10an
  127. ee10an
  128. e02
  129. e02an
  130. ee02an
  131. eel021old
  132. el021old
  133. eel132
  134. eel000cT
  135. eel0TT
  136. eelT00
  137. eelTTT
  138. eelT11
  139. eelT1
  140. eelT12
  141. eelTT1
  142. eelT01
  143. eel0T1
  144. eel12131
  145. eel2131
  146. eel3132
  147. eel0321old
  148. el0321old
  149. eel2122old
  150. el2122old
  151. eel0000
  152. eel00001
  153. eel00000
  154. eel11111
  155. e12
  156. e12an
  157. el12
  158. e20
  159. e20an
  160. ee20an
  161. e21
  162. e21an
  163. ee21an
  164. e333
  165. e33
  166. e33an
  167. ee33an
  168. e3
  169. e3bi
  170. e3bir
  171. e03
  172. ee03
  173. e03an
  174. ee03an
  175. e30
  176. ee30
  177. e30an
  178. ee30an
  179. e13
  180. e13an
  181. ee13an
  182. e31
  183. ee31
  184. e31an
  185. ee31an
  186. e23
  187. e23an
  188. ee23an
  189. e32
  190. ee32
  191. e32an
  192. ee32an
  193. e123
  194. ee123
  195. el123
  196. e233
  197. e323
  198. e000
  199. e00
  200. e00an
  201. eel00cT
  202. eelTT
  203. e0a
  204. eelT
  205. eel0cT
  206. eelT0
  207. e0bi
  208. e0bir
  209. uun0.1
  210. un0.1
  211. uunT1
  212. uunT1p1
  213. uunT21
  214. uun121
  215. uun121p1
  216. uun132
  217. uun132p1
  218. anabss7p1
  219. un10
  220. un01
  221. un2122
  222. uun2131
  223. uun2131p1
  224. uunTT1
  225. uunTT1p1
  226. uunTT1p2
  227. uunT11
  228. uunT11p1
  229. uunT11p2
  230. uunT12
  231. uunT12p1
  232. uunT12p2
  233. uunT12p3
  234. uunT12p4
  235. uunT12p5
  236. uun111
  237. 3anidm12p1
  238. 3anidm12p2
  239. uun123
  240. uun123p1
  241. uun123p2
  242. uun123p3
  243. uun123p4
  244. uun2221
  245. uun2221p1
  246. uun2221p2
  247. 3impdirp1
  248. 3impcombi