Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61da2ne Structured version   Visualization version   GIF version

Theorem pm2.61da2ne 2870
 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 747 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 678 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 2869 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 2869 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ≠ wne 2780 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 196  df-an 385  df-ne 2782 This theorem is referenced by:  pm2.61da3ne  2871  isabvd  18643  xrsxmet  22420  chordthmlem3  24361  mumul  24707  lgsdirnn0  24869  lgsdinn0  24870  eupath2lem3  26506  lfl1dim  33426  lfl1dim2N  33427  pmodlem2  34151  cdlemg29  35011  cdlemg39  35022  cdlemg44b  35038  dia2dimlem9  35379  dihprrn  35733  dvh3dim  35753  lcfl9a  35812  lclkrlem2l  35825  lcfrlem42  35891  mapdh6kN  36053  hdmap1l6k  36128
 Copyright terms: Public domain W3C validator