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 715 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 467 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3029 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3029 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  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 207  df-an 396  df-ne 2941
This theorem is referenced by:  pm2.61da3ne  3031  isabvd  20813  xrsxmet  24831  chordthmlem3  26877  mumul  27224  lgsdirnn0  27388  lgsdinn0  27389  constrrtcc  33776  lfl1dim  39122  lfl1dim2N  39123  pmodlem2  39849  cdlemg29  40707  cdlemg39  40718  cdlemg44b  40734  dia2dimlem9  41074  dihprrn  41428  dvh3dim  41448  lcfl9a  41507  lclkrlem2l  41520  lcfrlem42  41586  mapdh6kN  41748  hdmap1l6k  41822
  Copyright terms: Public domain W3C validator