Description: Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011) (Proof shortened by Wolf Lammen, 27-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nanbi1 | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi1 | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 → ¬ 𝜒 ) ↔ ( 𝜓 → ¬ 𝜒 ) ) ) | |
2 | dfnan2 | ⊢ ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜑 → ¬ 𝜒 ) ) | |
3 | dfnan2 | ⊢ ( ( 𝜓 ⊼ 𝜒 ) ↔ ( 𝜓 → ¬ 𝜒 ) ) | |
4 | 1 2 3 | 3bitr4g | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜒 ) ) ) |