Description: Theorem *4.14 of WhiteheadRussell p. 117. Related to con34b . (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 23-Oct-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pm4.14 | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( ( 𝜑 ∧ ¬ 𝜒 ) → ¬ 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con34b | ⊢ ( ( 𝜓 → 𝜒 ) ↔ ( ¬ 𝜒 → ¬ 𝜓 ) ) | |
| 2 | 1 | imbi2i | ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( 𝜑 → ( ¬ 𝜒 → ¬ 𝜓 ) ) ) |
| 3 | impexp | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) | |
| 4 | impexp | ⊢ ( ( ( 𝜑 ∧ ¬ 𝜒 ) → ¬ 𝜓 ) ↔ ( 𝜑 → ( ¬ 𝜒 → ¬ 𝜓 ) ) ) | |
| 5 | 2 3 4 | 3bitr4i | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( ( 𝜑 ∧ ¬ 𝜒 ) → ¬ 𝜓 ) ) |