Theorem pm2.61da2ne 3029

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ≠ wne 2939

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 206  df-an 397  df-ne 2940

This theorem is referenced by:  pm2.61da3ne  3030  isabvd  20335  xrsxmet  24209  chordthmlem3  26221  mumul  26567  lgsdirnn0  26729  lgsdinn0  26730  lfl1dim  37656  lfl1dim2N  37657  pmodlem2  38383  cdlemg29  39241  cdlemg39  39252  cdlemg44b  39268  dia2dimlem9  39608  dihprrn  39962  dvh3dim  39982  lcfl9a  40041  lclkrlem2l  40054  lcfrlem42  40120  mapdh6kN  40282  hdmap1l6k  40356