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

Theorem pm2.61da2ne 3087
Description: Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)
Hypotheses
Ref Expression
pm2.61da2ne.1 ((𝜑𝐴 = 𝐵) → 𝜓)
pm2.61da2ne.2 ((𝜑𝐶 = 𝐷) → 𝜓)
pm2.61da2ne.3 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
Assertion
Ref Expression
pm2.61da2ne (𝜑𝜓)

Proof of Theorem pm2.61da2ne
StepHypRef Expression
1 pm2.61da2ne.1 . 2 ((𝜑𝐴 = 𝐵) → 𝜓)
2 pm2.61da2ne.2 . . . 4 ((𝜑𝐶 = 𝐷) → 𝜓)
32adantlr 706 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 461 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3086 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3086 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1656  wne 2999
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 199  df-an 387  df-ne 3000
This theorem is referenced by:  pm2.61da3ne  3088  isabvd  19183  xrsxmet  22989  chordthmlem3  24981  mumul  25327  lgsdirnn0  25489  lgsdinn0  25490  lfl1dim  35191  lfl1dim2N  35192  pmodlem2  35917  cdlemg29  36775  cdlemg39  36786  cdlemg44b  36802  dia2dimlem9  37142  dihprrn  37496  dvh3dim  37516  lcfl9a  37575  lclkrlem2l  37588  lcfrlem42  37654  mapdh6kN  37816  hdmap1l6k  37890
  Copyright terms: Public domain W3C validator