View source for Template:Transformation rules

{{Sidebar
| class = plainlist
| title = [[Rule of inference|Transformation rules]]

   | headingstyle = background:#eaeaff;
   | contentstyle = padding-top:0.15em;

| heading1style =  background:#ddf;font-size:110%; border-bottom:1px #fefefe solid;
| heading1 = [[Propositional calculus]]

   | heading2 = [[Rule of inference|Rules of inference]]
   | content2 =
*   [[Conditional proof|<span>Implication introduction</span>]]{{\}}<!--
 -->[[Modus ponens|<span title="A→B, &nbsp; A &nbsp; ⊢ &nbsp; B">elimination (''modus ponens'')</span>]]
*   [[Biconditional introduction|<span title="A→B, &nbsp; B→A &nbsp; ⊢ &nbsp; A↔B">Biconditional introduction</span>]]{{\}}<!--
 -->[[Biconditional elimination|<span title="A↔B &nbsp; ⊢ &nbsp; A→B"><!--Biconditional -->elimination</span>]]
*   [[Conjunction introduction|<span title="A, &nbsp; B &nbsp; ⊢ &nbsp; A∧B">Conjunction introduction</span>]]{{\}}<!--
 -->[[Conjunction elimination|<span title="A∧B &nbsp; ⊢ &nbsp; A">elimination</span>]]
*   [[Disjunction introduction|<span title="A &nbsp; ⊢ &nbsp; A∨B">Disjunction introduction</span>]]{{\}}<!--
 -->[[Disjunction elimination|<span title="A∨B, &nbsp; A→C, &nbsp; B→C &nbsp; ⊢ &nbsp; C"><!--Disjunction -->elimination</span>]]
*   [[Disjunctive syllogism|<span title="A∨B, &nbsp; ¬A &nbsp; ⊢ &nbsp; B">Disjunctive<!-- syllogism--></span>]]{{\}}<!--
 -->[[Hypothetical syllogism|<span title="A→B, &nbsp; B→C &nbsp; ⊢ &nbsp; A→C">hypothetical syllogism</span>]]
*   [[Constructive dilemma|<span title="A→P, &nbsp; B→Q, &nbsp; A∨B &nbsp; ⊢ &nbsp; P∨Q">Constructive<!-- dilemma--></span>]]{{\}}<!--
 -->[[Destructive dilemma|<span title="A→P, &nbsp; B→Q, &nbsp; ¬P∨¬Q &nbsp; ⊢ &nbsp; ¬A∨¬B">destructive dilemma</span>]]
*   [[Absorption (logic)|<span title="A→B &nbsp; ⊢ &nbsp; A→A∧B">Absorption</span>]]{{\}}<!--
 -->[[Modus tollens|<span title="A→B, &nbsp; ¬B &nbsp; ⊢ &nbsp; ¬A">''modus tollens''</span>]]{{\}}<!--
 -->[[Modus ponendo tollens|<span title="¬(A∧B), &nbsp; A &nbsp; ⊢ &nbsp; ¬B">''modus ponendo tollens''</span>]]
* [[Negation introduction]]
   | heading3 = [[Rule of replacement|Rules of replacement]]
   | content3 = {{Flatlist}}
* [[Associative property#Propositional logic|<span title="A∨(B∨C) &nbsp; = &nbsp; (A∨B)∨C">Associativity</span>]]
* [[Commutative property#Propositional logic|<span title="A∨B &nbsp; = &nbsp; B∨A">Commutativity</span>]]
* [[Distributive property#Propositional logic|<span title="A∧(B∨C) &nbsp; = &nbsp; (A∧B)∨(A∧C)">Distributivity</span>]]
* [[Double negation|<span title="¬¬A &nbsp; = &nbsp; A">Double negation</span>]]
* [[De Morgan's laws]]
* [[Transposition (logic)|Transposition]]
* [[Material implication (rule of inference)|<span title="A→B &nbsp; ⊢ &nbsp; ¬A∨B">Material implication</span>]]
* [[Exportation (logic)|<span title="(A∧B)→C &nbsp; ⊢ &nbsp; A→(B→C)">Exportation</span>]]
* [[Tautology (rule of inference)|<span title="A∨A &nbsp; = &nbsp; A">Tautology</span>]]
{{endflatlist}}

| heading4style = background:#ddf;font-size:110%;
| heading4 = [[First-order logic|Predicate logic]]
   | heading5 = [[Rule of inference|Rules of inference]]
   | content5 =
* [[Universal generalization]]{{\}}[[Universal instantiation|instantiation]]
* [[Existential generalization]]{{\}}[[Existential instantiation|instantiation]]

}}<noinclude>{{doc|content=

===See also===
* {{Template link|Classical logic}}
* {{Template link|Logic templates}}

[[Category:Logic templates]]
[[Category:Mathematics sidebar templates]]
[[Category:Philosophy and thinking sidebar templates]]
}}</noinclude>