Theorem pm2.61da2ne 3013

Description: Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)

Hypotheses

Ref	Expression
pm2.61da2ne.1	⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)
pm2.61da2ne.2	⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)
pm2.61da2ne.3	⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓)

Assertion

Ref	Expression
pm2.61da2ne	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.61da2ne

Step	Hyp	Ref	Expression
1		pm2.61da2ne.1	. 2 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)
2		pm2.61da2ne.2	. . . 4 ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓)
3	2	adantlr 715	. . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4		pm2.61da2ne.3	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓)
5	4	anassrs 467	. . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ≠ 𝐷) → 𝜓)
6	3, 5	pm2.61dane 3012	. 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
7	1, 6	pm2.61dane 3012	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-ne 2926

This theorem is referenced by:  pm2.61da3ne  3014  isabvd  20697  xrsxmet  24696  chordthmlem3  26742  mumul  27089  lgsdirnn0  27253  lgsdinn0  27254  constrrtcc  33708  lfl1dim  39110  lfl1dim2N  39111  pmodlem2  39836  cdlemg29  40694  cdlemg39  40705  cdlemg44b  40721  dia2dimlem9  41061  dihprrn  41415  dvh3dim  41435  lcfl9a  41494  lclkrlem2l  41507  lcfrlem42  41573  mapdh6kN  41735  hdmap1l6k  41809