Theorem pm2.61da2ne 3043

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2956

This theorem is used by:  pm2.61da3ne  3044  isabvd  20981  xrsxmet  25039  chordthmlem3  27074  mumul  27420  lgsdirnn0  27583  lgsdinn0  27584  constrrtcc  34248  lfl1dim  39997  lfl1dim2N  39998  pmodlem2  40723  cdlemg29  41581  cdlemg39  41592  cdlemg44b  41608  dia2dimlem9  41948  dihprrn  42302  dvh3dim  42322  lcfl9a  42381  lclkrlem2l  42394  lcfrlem42  42460  mapdh6kN  42622  hdmap1l6k  42696