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 3031
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 694 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 458 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3030 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3030 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wne 2943
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 197  df-an 383  df-ne 2944
This theorem is referenced by:  pm2.61da3ne  3032  isabvd  19030  xrsxmet  22832  chordthmlem3  24782  mumul  25128  lgsdirnn0  25290  lgsdinn0  25291  lfl1dim  34930  lfl1dim2N  34931  pmodlem2  35655  cdlemg29  36514  cdlemg39  36525  cdlemg44b  36541  dia2dimlem9  36882  dihprrn  37236  dvh3dim  37256  lcfl9a  37315  lclkrlem2l  37328  lcfrlem42  37394  mapdh6kN  37556  hdmap1l6k  37630
  Copyright terms: Public domain W3C validator