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 3030
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 468 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3029 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3029 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wne 2940
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 397  df-ne 2941
This theorem is referenced by:  pm2.61da3ne  3031  isabvd  20432  xrsxmet  24332  chordthmlem3  26346  mumul  26692  lgsdirnn0  26854  lgsdinn0  26855  lfl1dim  38083  lfl1dim2N  38084  pmodlem2  38810  cdlemg29  39668  cdlemg39  39679  cdlemg44b  39695  dia2dimlem9  40035  dihprrn  40389  dvh3dim  40409  lcfl9a  40468  lclkrlem2l  40481  lcfrlem42  40547  mapdh6kN  40709  hdmap1l6k  40783
  Copyright terms: Public domain W3C validator