This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Negated equality and membership Negated equality pm2.61ne
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM , 24-May-2006) (Proof shortened by Andrew Salmon , 25-May-2011)
(Proof shortened by Wolf Lammen , 25-Nov-2019)
Ref
Expression
Hypotheses
pm2.61ne.1 ⊢ ( 𝐴 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
pm2.61ne.2 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝜓 )
pm2.61ne.3 ⊢ ( 𝜑 → 𝜒 )
Assertion
pm2.61ne ⊢ ( 𝜑 → 𝜓 )
Proof
Step
Hyp
Ref
Expression
1
pm2.61ne.1 ⊢ ( 𝐴 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
2
pm2.61ne.2 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝜓 )
3
pm2.61ne.3 ⊢ ( 𝜑 → 𝜒 )
4
3 1
imbitrrid ⊢ ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) )
5
2
expcom ⊢ ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) )
6
4 5
pm2.61ine ⊢ ( 𝜑 → 𝜓 )