MPE Home 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  |-  ( (
ph  /\  A  =  B )  ->  ps )
pm2.61da2ne.2  |-  ( (
ph  /\  C  =  D )  ->  ps )
pm2.61da2ne.3  |-  ( (
ph  /\  ( A  =/=  B  /\  C  =/= 
D ) )  ->  ps )
Assertion
Ref Expression
pm2.61da2ne  |-  ( ph  ->  ps )

Proof of Theorem pm2.61da2ne
StepHypRef Expression
1 pm2.61da2ne.1 . 2  |-  ( (
ph  /\  A  =  B )  ->  ps )
2 pm2.61da2ne.2 . . . 4  |-  ( (
ph  /\  C  =  D )  ->  ps )
32adantlr 696 . . 3  |-  ( ( ( ph  /\  A  =/=  B )  /\  C  =  D )  ->  ps )
4 pm2.61da2ne.3 . . . 4  |-  ( (
ph  /\  ( A  =/=  B  /\  C  =/= 
D ) )  ->  ps )
54anassrs 630 . . 3  |-  ( ( ( ph  /\  A  =/=  B )  /\  C  =/=  D )  ->  ps )
63, 5pm2.61dane 2676 . 2  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
71, 6pm2.61dane 2676 1  |-  ( ph  ->  ps )
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