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 714 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 469 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3029 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3029 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  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 206  df-an 398  df-ne 2941
This theorem is referenced by:  pm2.61da3ne  3031  isabvd  20293  xrsxmet  24188  chordthmlem3  26200  mumul  26546  lgsdirnn0  26708  lgsdinn0  26709  lfl1dim  37629  lfl1dim2N  37630  pmodlem2  38356  cdlemg29  39214  cdlemg39  39225  cdlemg44b  39241  dia2dimlem9  39581  dihprrn  39935  dvh3dim  39955  lcfl9a  40014  lclkrlem2l  40027  lcfrlem42  40093  mapdh6kN  40255  hdmap1l6k  40329
  Copyright terms: Public domain W3C validator