Metamath Proof Explorer


Table of Contents - 1.2.5. Logical equivalence

The definition df-bi in this section is our first definition, which introduces and defines the biconditional connective used to denote logical equivalence. We define a wff of the form as an abbreviation for .

Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as". Instead, we will later use the biconditional connective for this purpose (df-an is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions.

A note on definitions: definitions are required to be eliminable (that is, a theorem stated in terms of the defined symbol can also be stated without it) and conservative (that is, a theorem whose statement does not contain the defined symbol can be proved without using that definition). This means that a definition does not increase the expressive power nor the deductive power, respectively, of a theory. On the other hand, definitions are often useful to write shorter proofs, so in (i)set.mm we will generally not try to avoid them. This is why, for instance, some theorems which do not contain disjunction in their statement are placed after the section on disjunction because a shorter proof using disjunction is possible.

  1. wb
  2. df-bi
  3. impbi
  4. impbii
  5. impbidd
  6. impbid21d
  7. impbid
  8. dfbi1
  9. dfbi1ALT
  10. biimp
  11. biimpi
  12. sylbi
  13. sylib
  14. sylbb
  15. biimpr
  16. bicom1
  17. bicom
  18. bicomd
  19. bicomi
  20. impbid1
  21. impbid2
  22. impcon4bid
  23. biimpri
  24. biimpd
  25. mpbi
  26. mpbir
  27. mpbid
  28. mpbii
  29. sylibr
  30. sylbir
  31. sylbbr
  32. sylbb1
  33. sylbb2
  34. sylibd
  35. sylbid
  36. mpbidi
  37. syl5bi
  38. syl5bir
  39. syl5ib
  40. syl5ibcom
  41. syl5ibr
  42. syl5ibrcom
  43. biimprd
  44. biimpcd
  45. biimprcd
  46. syl6ib
  47. syl6ibr
  48. syl6bi
  49. syl6bir
  50. syl7bi
  51. syl8ib
  52. mpbird
  53. mpbiri
  54. sylibrd
  55. sylbird
  56. biid
  57. biidd
  58. pm5.1im
  59. 2th
  60. 2thd
  61. monothetic
  62. ibi
  63. ibir
  64. ibd
  65. pm5.74
  66. pm5.74i
  67. pm5.74ri
  68. pm5.74d
  69. pm5.74rd
  70. bitri
  71. bitr2i
  72. bitr3i
  73. bitr4i
  74. bitrd
  75. bitr2d
  76. bitr3d
  77. bitr4d
  78. syl5bb
  79. syl5rbb
  80. syl5bbr
  81. syl5rbbr
  82. syl6bb
  83. syl6rbb
  84. syl6bbr
  85. syl6rbbr
  86. 3imtr3i
  87. 3imtr4i
  88. 3imtr3d
  89. 3imtr4d
  90. 3imtr3g
  91. 3imtr4g
  92. 3bitri
  93. 3bitrri
  94. 3bitr2i
  95. 3bitr2ri
  96. 3bitr3i
  97. 3bitr3ri
  98. 3bitr4i
  99. 3bitr4ri
  100. 3bitrd
  101. 3bitrrd
  102. 3bitr2d
  103. 3bitr2rd
  104. 3bitr3d
  105. 3bitr3rd
  106. 3bitr4d
  107. 3bitr4rd
  108. 3bitr3g
  109. 3bitr4g
  110. notnotb
  111. con34b
  112. con4bid
  113. notbid
  114. notbi
  115. notbii
  116. con4bii
  117. mtbi
  118. mtbir
  119. mtbid
  120. mtbird
  121. mtbii
  122. mtbiri
  123. sylnib
  124. sylnibr
  125. sylnbi
  126. sylnbir
  127. xchnxbi
  128. xchnxbir
  129. xchbinx
  130. xchbinxr
  131. imbi2i
  132. jcndOLD
  133. bibi2i
  134. bibi1i
  135. bibi12i
  136. imbi2d
  137. imbi1d
  138. bibi2d
  139. bibi1d
  140. imbi12d
  141. bibi12d
  142. imbi12
  143. imbi1
  144. imbi2
  145. imbi1i
  146. imbi12i
  147. bibi1
  148. bitr3
  149. con2bi
  150. con2bid
  151. con1bid
  152. con1bii
  153. con2bii
  154. con1b
  155. con2b
  156. biimt
  157. pm5.5
  158. a1bi
  159. mt2bi
  160. mtt
  161. imnot
  162. pm5.501
  163. ibib
  164. ibibr
  165. tbt
  166. nbn2
  167. bibif
  168. nbn
  169. nbn3
  170. pm5.21im
  171. 2false
  172. 2falsed
  173. 2falsedOLD
  174. pm5.21ni
  175. pm5.21nii
  176. pm5.21ndd
  177. bija
  178. pm5.18
  179. xor3
  180. nbbn
  181. biass
  182. biluk
  183. pm5.19
  184. bi2.04
  185. pm5.4
  186. imdi
  187. pm5.41
  188. pm4.8
  189. pm4.81
  190. imim21b