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 3028
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 715 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 467 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3027 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3027 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wne 2938
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 207  df-an 396  df-ne 2939
This theorem is referenced by:  pm2.61da3ne  3029  isabvd  20830  xrsxmet  24845  chordthmlem3  26892  mumul  27239  lgsdirnn0  27403  lgsdinn0  27404  constrrtcc  33741  lfl1dim  39103  lfl1dim2N  39104  pmodlem2  39830  cdlemg29  40688  cdlemg39  40699  cdlemg44b  40715  dia2dimlem9  41055  dihprrn  41409  dvh3dim  41429  lcfl9a  41488  lclkrlem2l  41501  lcfrlem42  41567  mapdh6kN  41729  hdmap1l6k  41803
  Copyright terms: Public domain W3C validator