Theorem pm2.61da2ne 3021

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  pm2.61da3ne  3022  isabvd  20760  xrsxmet  24769  chordthmlem3  26815  mumul  27162  lgsdirnn0  27326  lgsdinn0  27327  constrrtcc  33917  lfl1dim  39501  lfl1dim2N  39502  pmodlem2  40227  cdlemg29  41085  cdlemg39  41096  cdlemg44b  41112  dia2dimlem9  41452  dihprrn  41806  dvh3dim  41826  lcfl9a  41885  lclkrlem2l  41898  lcfrlem42  41964  mapdh6kN  42126  hdmap1l6k  42200