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

Theorem pm2.61da2ne 2715
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 712 . . 3  |-  ( ( ( ph  /\  A  =/=  B )  /\  C  =  D )  ->  ps )
4 pm2.61da2ne.3 . . . 4  |-  ( (
ph  /\  ( A  =/=  B  /\  C  =/= 
D ) )  ->  ps )
54anassrs 646 . . 3  |-  ( ( ( ph  /\  A  =/=  B )  /\  C  =/=  D )  ->  ps )
63, 5pm2.61dane 2714 . 2  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
71, 6pm2.61dane 2714 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399    =/= wne 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-ne 2593
This theorem is referenced by:  pm2.61da3ne  2716  pm2.61da3neOLD  2717  isabvd  17605  xrsxmet  21422  chordthmlem3  23304  mumul  23595  lgsdirnn0  23754  lgsdinn0  23755  eupath2lem3  25125  lfl1dim  35298  lfl1dim2N  35299  pmodlem2  36023  cdlemg29  36883  cdlemg39  36894  cdlemg44b  36910  dia2dimlem9  37251  dihprrn  37605  dvh3dim  37625  lcfl9a  37684  lclkrlem2l  37697  lcfrlem42  37763  mapdh6kN  37925  hdmap1l6k  38000
  Copyright terms: Public domain W3C validator