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