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

Theorem pm2.61da2ne 2538
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 695 . . 3  |-  ( ( ( ph  /\  A  =/=  B )  /\  C  =  D )  ->  ps )
4 pm2.61da2ne.3 . . . 4  |-  ( (
ph  /\  ( A  =/=  B  /\  C  =/= 
D ) )  ->  ps )
54anassrs 629 . . 3  |-  ( ( ( ph  /\  A  =/=  B )  /\  C  =/=  D )  ->  ps )
63, 5pm2.61dane 2537 . 2  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
71, 6pm2.61dane 2537 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    =/= wne 2459
This theorem is referenced by:  pm2.61da3ne  2539  isabvd  15601  xrsxmet  18331  chordthmlem3  20147  mumul  20435  lgsdirnn0  20594  lgsdinn0  20595  eupath2lem3  23918  lfl1dim  29933  lfl1dim2N  29934  pmodlem2  30658  cdlemg29  31516  cdlemg39  31527  cdlemg44b  31543  dia2dimlem9  31884  dihprrn  32238  dvh3dim  32258  lcfl9a  32317  lclkrlem2l  32330  lcfrlem42  32396  mapdh6kN  32558  hdmap1l6k  32633
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 177  df-an 360  df-ne 2461
  Copyright terms: Public domain W3C validator