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 2866
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 746 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 677 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 2865 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 2865 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wne 2776
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 195  df-an 384  df-ne 2778
This theorem is referenced by:  pm2.61da3ne  2867  isabvd  18586  xrsxmet  22349  chordthmlem3  24275  mumul  24621  lgsdirnn0  24783  lgsdinn0  24784  eupath2lem3  26269  lfl1dim  33226  lfl1dim2N  33227  pmodlem2  33951  cdlemg29  34811  cdlemg39  34822  cdlemg44b  34838  dia2dimlem9  35179  dihprrn  35533  dvh3dim  35553  lcfl9a  35612  lclkrlem2l  35625  lcfrlem42  35691  mapdh6kN  35853  hdmap1l6k  35928
  Copyright terms: Public domain W3C validator