MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61da2ne Structured version   Visualization version   GIF version

Theorem pm2.61da2ne 3102
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
StepHypRef Expression
1 pm2.61da2ne.1 . 2 ((𝜑𝐴 = 𝐵) → 𝜓)
2 pm2.61da2ne.2 . . . 4 ((𝜑𝐶 = 𝐷) → 𝜓)
32adantlr 714 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 471 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3101 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3101 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wne 3014
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 400  df-ne 3015
This theorem is referenced by:  pm2.61da3ne  3103  isabvd  19591  xrsxmet  23420  chordthmlem3  25426  mumul  25772  lgsdirnn0  25934  lgsdinn0  25935  lfl1dim  36365  lfl1dim2N  36366  pmodlem2  37091  cdlemg29  37949  cdlemg39  37960  cdlemg44b  37976  dia2dimlem9  38316  dihprrn  38670  dvh3dim  38690  lcfl9a  38749  lclkrlem2l  38762  lcfrlem42  38828  mapdh6kN  38990  hdmap1l6k  39064
  Copyright terms: Public domain W3C validator