Description: Obsolete version of ifpn as of 5-May-2024. (Contributed by BJ, 30-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ifpnOLD | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( ¬ 𝜑 , 𝜒 , 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | notnotb | ⊢ ( 𝜑 ↔ ¬ ¬ 𝜑 ) | |
| 2 | 1 | imbi1i | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ ¬ 𝜑 → 𝜓 ) ) |
| 3 | 2 | anbi2ci | ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ↔ ( ( ¬ 𝜑 → 𝜒 ) ∧ ( ¬ ¬ 𝜑 → 𝜓 ) ) ) |
| 4 | dfifp2 | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) | |
| 5 | dfifp2 | ⊢ ( if- ( ¬ 𝜑 , 𝜒 , 𝜓 ) ↔ ( ( ¬ 𝜑 → 𝜒 ) ∧ ( ¬ ¬ 𝜑 → 𝜓 ) ) ) | |
| 6 | 3 4 5 | 3bitr4i | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ if- ( ¬ 𝜑 , 𝜒 , 𝜓 ) ) |