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

Theorem pm2.61da2ne 2525
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 2524 . 2  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
71, 6pm2.61dane 2524 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    =/= wne 2446
This theorem is referenced by:  pm2.61da3ne  2526  isabvd  15585  xrsxmet  18315  chordthmlem3  20131  mumul  20419  lgsdirnn0  20578  lgsdinn0  20579  eupath2lem3  23903  lfl1dim  29311  lfl1dim2N  29312  pmodlem2  30036  cdlemg29  30894  cdlemg39  30905  cdlemg44b  30921  dia2dimlem9  31262  dihprrn  31616  dvh3dim  31636  lcfl9a  31695  lclkrlem2l  31708  lcfrlem42  31774  mapdh6kN  31936  hdmap1l6k  32011
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 2448
  Copyright terms: Public domain W3C validator