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 3102
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 711 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 468 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3101 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3101 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wne 3013
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 208  df-an 397  df-ne 3014
This theorem is referenced by:  pm2.61da3ne  3103  isabvd  19520  xrsxmet  23344  chordthmlem3  25339  mumul  25685  lgsdirnn0  25847  lgsdinn0  25848  lfl1dim  36137  lfl1dim2N  36138  pmodlem2  36863  cdlemg29  37721  cdlemg39  37732  cdlemg44b  37748  dia2dimlem9  38088  dihprrn  38442  dvh3dim  38462  lcfl9a  38521  lclkrlem2l  38534  lcfrlem42  38600  mapdh6kN  38762  hdmap1l6k  38836
  Copyright terms: Public domain W3C validator