Editing Material conditional (section)

==A selection of theorems (classical logic)==
In [[classical logic]] material implication validates the following:
<div style="margin-left: 20px;">
{{collapse top
| title=<span style="display:block; text-align:left; margin-left: -50px; padding-left: 0;">Contraposition: <math>(\neg Q \to \neg P) \to (P \to Q)</math></span>
| bg=#ffffff | fg=#000000
}}
{|
|1.{{spaces|1}}
|[ (Q → ⊥) → (P → ⊥) ]
|{{spaces|1}}// Assume (to discharge at 9)
|-
|2.{{spaces|1}}
|[ P ]
|{{spaces|1}}// Assume (to discharge at 8)
|-
|3.{{spaces|1}}
|[ Q → ⊥ ]
|{{spaces|1}}// Assume (to discharge at 6))
|-
|4.{{spaces|1}}
|P → ⊥
|{{spaces|1}}// <math>\to</math>E (1, 3)
|-
|5.{{spaces|1}}
|⊥ 
|{{spaces|1}}// <math>\to</math>E (2, 4)
|-
|6.{{spaces|1}}
|(Q → ⊥) → ⊥ 
|{{spaces|1}}// <math>\to</math>I (3, 5) (discharging 3)
|-
|7.{{spaces|1}}
|Q 
|{{spaces|1}}// <math>\neg\neg</math>E (6)
|-
|8.{{spaces|1}}
|P → Q 
|{{spaces|1}}// <math>\to</math>I (2, 7) (discharging 2)
|-
|9.{{spaces|1}}
|((Q → ⊥) → (P → ⊥)) → (P → Q)
|{{spaces|1}}// <math>\to</math>I (1, 8) (discharging 1)
|}
{{collapse bottom}}
</div>
<div style="margin-left: 20px;">
{{collapse top
| title=<span style="display:block; text-align:left; margin-left: -50px; padding-left: 0;">[[Peirce's law]]: <math>((P \to Q) \to P) \to P</math></span>
| bg=#ffffff | fg=#000000
}}
{|
|1.{{spaces|1}}
|[ (P → Q) → P ]
|{{spaces|1}}// Assume (to discharge at 11)
|-
|2.{{spaces|1}}
|[ P → ⊥ ]
|{{spaces|1}}// Assume (to discharge at 9)
|-
|3.{{spaces|1}}
|[ P ]
|{{spaces|1}}// Assume (to discharge at 6)
|-
|4.{{spaces|1}}
|⊥
|{{spaces|1}}// <math>\to</math>E (2, 3)
|-
|5.{{spaces|1}}
|Q 
|{{spaces|1}}// <math>\bot</math>E (4)
|-
|6.{{spaces|1}}
|P → Q 
|{{spaces|1}}// <math>\to</math>I (3, 5) (discharging 3)
|-
|7.{{spaces|1}}
|P
|{{spaces|1}}// <math>\to</math>E (1, 6)
|-
|8.{{spaces|1}}
|⊥
|{{spaces|1}}// <math>\to</math>E (2, 7)
|-
|9.{{spaces|1}}
|(P → ⊥) → ⊥
|{{spaces|1}}// <math>\to</math>I (2, 8) (discharging 2)
|-
|10.{{spaces|1}}
|P
|{{spaces|1}}// <math>\neg \neg</math>E (9)
|-
|11.{{spaces|1}}
|((P → Q) → P) → P
|{{spaces|1}}// <math>\to</math>I (1, 10) (discharging 1)
|}
{{collapse bottom}}
</div>
<div style="margin-left: 20px;">
{{collapse top
| title=<span style="display:block; text-align:left; margin-left: -50px; padding-left: 0;">[[Vacuous truth|Vacuous conditional]] (IPC): <math>\neg P \to (P \to Q)</math></span>
| bg=#ffffff | fg=#000000
}}
{|
|1.{{spaces|1}}
|<math>[ P \to \bot ]</math>
|{{spaces|1}}// Assume
|-
|2.{{spaces|1}}
|<math>[ P ]</math>
|{{spaces|1}}// Assume
|-
|3.{{spaces|1}}
| <math>\bot</math>
|{{spaces|1}}// <math>\to</math>E (1, 2)
|-
|4.{{spaces|1}}
|<math>Q</math>
|{{spaces|1}}// <math>\bot</math>E (3)
|-
|5.{{spaces|1}}
|<math>P \to Q</math>
|{{spaces|1}}// <math>\to </math>I (2, 4) (discharging 2)
|-
|6.{{spaces|1}}
|<math>( P \to \bot ) \to ( P \to Q )</math> 
|{{spaces|1}}// <math>\to </math>I (1, 5) (discharging 1)
|}
{{collapse bottom}}
</div>
* [[Import-Export (logic)|Import-export]]: <math>P \to (Q \to R) \equiv (P \land Q) \to R</math>
* Negated conditionals: <math>\neg(P \to Q) \equiv P \land \neg Q</math>
* Or-and-if: <math>P \to Q \equiv \neg P \lor Q</math>
* Commutativity of antecedents: <math>\big(P \to (Q \to R)\big) \equiv \big(Q \to (P \to R)\big)</math>
* [[Left distributivity]]: <math>\big(R \to (P \to Q)\big) \equiv \big((R \to P) \to (R \to Q)\big)</math>

Similarly, on classical interpretations of the other connectives, material implication validates the following [[Logical consequence#Semantic consequence|entailment]]s:
* Antecedent strengthening: <math>P \to Q \models (P \land R) \to Q</math>
* [[transitive relation|Transitivity]]: <math>(P \to Q) \land (Q \to R) \models P \to R</math>
* [[Simplification of disjunctive antecedents]]: <math>(P \lor Q) \to R \models (P \to R) \land (Q \to R)</math>

[[Tautology (logic)|Tautologies]] involving material implication include:
* [[reflexive relation|Reflexivity]]: <math>\models P \to P</math>
* [[connex relation|Totality]]: <math>\models (P \to Q) \lor (Q \to P)</math>
* [[Law of excluded middle|Conditional excluded middle]]: <math>\models (P \to Q) \lor (P \to \neg Q)</math>