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 3026
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 713 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 466 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3025 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3025 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wne 2936
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 206  df-an 395  df-ne 2937
This theorem is referenced by:  pm2.61da3ne  3027  isabvd  20705  xrsxmet  24743  chordthmlem3  26784  mumul  27131  lgsdirnn0  27295  lgsdinn0  27296  lfl1dim  38597  lfl1dim2N  38598  pmodlem2  39324  cdlemg29  40182  cdlemg39  40193  cdlemg44b  40209  dia2dimlem9  40549  dihprrn  40903  dvh3dim  40923  lcfl9a  40982  lclkrlem2l  40995  lcfrlem42  41061  mapdh6kN  41223  hdmap1l6k  41297
  Copyright terms: Public domain W3C validator