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

Theorem pm2.61da2ne 2677
 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
4 pm2.61da2ne.3 . . . 4
54anassrs 630 . . 3
63, 5pm2.61dane 2676 . 2
71, 6pm2.61dane 2676 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   wceq 1652   wne 2598 This theorem is referenced by:  pm2.61da3ne  2678  isabvd  15900  xrsxmet  18832  chordthmlem3  20667  mumul  20956  lgsdirnn0  21115  lgsdinn0  21116  eupath2lem3  21693  lfl1dim  29856  lfl1dim2N  29857  pmodlem2  30581  cdlemg29  31439  cdlemg39  31450  cdlemg44b  31466  dia2dimlem9  31807  dihprrn  32161  dvh3dim  32181  lcfl9a  32240  lclkrlem2l  32253  lcfrlem42  32319  mapdh6kN  32481  hdmap1l6k  32556 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178  df-an 361  df-ne 2600
 Copyright terms: Public domain W3C validator