Theorem pm2.61da2ne 3046

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 727	. . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4		pm2.61da2ne.3	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓)
5	4	anassrs 472	. . 3 ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ≠ 𝐷) → 𝜓)
6	3, 5	pm2.61dane 3045	. 2 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
7	1, 6	pm2.61dane 3045	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ≠ wne 2958

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 210  df-an 401  df-ne 2959

This theorem is referenced by:  pm2.61da3ne  3047  isabvd  20915  xrsxmet  24967  chordthmlem3  26999  mumul  27345  lgsdirnn0  27508  lgsdinn0  27509  constrrtcc  34125  lfl1dim  39915  lfl1dim2N  39916  pmodlem2  40641  cdlemg29  41499  cdlemg39  41510  cdlemg44b  41526  dia2dimlem9  41866  dihprrn  42220  dvh3dim  42240  lcfl9a  42299  lclkrlem2l  42312  lcfrlem42  42378  mapdh6kN  42540  hdmap1l6k  42614