Description: Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nanbii.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
Assertion | nanbi2i | ⊢ ( ( 𝜒 ⊼ 𝜑 ) ↔ ( 𝜒 ⊼ 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nanbii.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
2 | nanbi2 | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜒 ⊼ 𝜑 ) ↔ ( 𝜒 ⊼ 𝜓 ) ) ) | |
3 | 1 2 | ax-mp | ⊢ ( ( 𝜒 ⊼ 𝜑 ) ↔ ( 𝜒 ⊼ 𝜓 ) ) |