Description: Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | abciffcbatnabciffncbai.1 | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) | |
| Assertion | abciffcbatnabciffncbai | ⊢ ( ¬ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → ¬ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abciffcbatnabciffncbai.1 | ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) | |
| 2 | notbi | ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) ↔ ( ¬ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ¬ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) ) | |
| 3 | 2 | biimpi | ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) → ( ¬ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ¬ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) ) |
| 4 | 1 3 | ax-mp | ⊢ ( ¬ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ↔ ¬ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) |
| 5 | 4 | biimpi | ⊢ ( ¬ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → ¬ ( ( 𝜒 ∧ 𝜓 ) ∧ 𝜑 ) ) |