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

Theorem pm2.61da2ne 2622
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 2621 . 2  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
71, 6pm2.61dane 2621 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    =/= wne 2543
This theorem is referenced by:  pm2.61da3ne  2623  isabvd  15828  xrsxmet  18704  chordthmlem3  20535  mumul  20824  lgsdirnn0  20983  lgsdinn0  20984  eupath2lem3  21542  lfl1dim  29287  lfl1dim2N  29288  pmodlem2  30012  cdlemg29  30870  cdlemg39  30881  cdlemg44b  30897  dia2dimlem9  31238  dihprrn  31592  dvh3dim  31612  lcfl9a  31671  lclkrlem2l  31684  lcfrlem42  31750  mapdh6kN  31912  hdmap1l6k  31987
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 2545
  Copyright terms: Public domain W3C validator