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 714 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶 = 𝐷) → 𝜓)
4 pm2.61da2ne.3 . . . 4 ((𝜑 ∧ (𝐴𝐵𝐶𝐷)) → 𝜓)
54anassrs 469 . . 3 (((𝜑𝐴𝐵) ∧ 𝐶𝐷) → 𝜓)
63, 5pm2.61dane 3030 . 2 ((𝜑𝐴𝐵) → 𝜓)
71, 6pm2.61dane 3030 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wne 2941
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 2942
This theorem is referenced by:  pm2.61da3ne  3032  isabvd  20428  xrsxmet  24325  chordthmlem3  26339  mumul  26685  lgsdirnn0  26847  lgsdinn0  26848  lfl1dim  37991  lfl1dim2N  37992  pmodlem2  38718  cdlemg29  39576  cdlemg39  39587  cdlemg44b  39603  dia2dimlem9  39943  dihprrn  40297  dvh3dim  40317  lcfl9a  40376  lclkrlem2l  40389  lcfrlem42  40455  mapdh6kN  40617  hdmap1l6k  40691
  Copyright terms: Public domain W3C validator