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

Theorem pm2.61da3ne 2678
 Description: Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.)
Hypotheses
Ref Expression
pm2.61da3ne.1
pm2.61da3ne.2
pm2.61da3ne.3
pm2.61da3ne.4
Assertion
Ref Expression
pm2.61da3ne

Proof of Theorem pm2.61da3ne
StepHypRef Expression
1 pm2.61da3ne.1 . 2
2 pm2.61da3ne.2 . 2
3 pm2.61da3ne.3 . . . 4
5 simpll 731 . . . 4
6 simplrl 737 . . . 4
7 simplrr 738 . . . 4
8 simpr 448 . . . 4
9 pm2.61da3ne.4 . . . 4
105, 6, 7, 8, 9syl13anc 1186 . . 3
114, 10pm2.61dane 2676 . 2
121, 2, 11pm2.61da2ne 2677 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936   wceq 1652   wne 2598 This theorem is referenced by:  trljco  31474  dvh4dimN  32182 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-3an 938  df-ne 2600
 Copyright terms: Public domain W3C validator