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

Theorem ssltsepcd 27155
Description: Two elements of separated sets obey less-than. Deduction form of ssltsepc 27154. (Contributed by Scott Fenton, 25-Sep-2024.)
Hypotheses
Ref Expression
ssltsepcd.1 (𝜑𝐴 <<s 𝐵)
ssltsepcd.2 (𝜑𝑋𝐴)
ssltsepcd.3 (𝜑𝑌𝐵)
Assertion
Ref Expression
ssltsepcd (𝜑𝑋 <s 𝑌)

Proof of Theorem ssltsepcd
StepHypRef Expression
1 ssltsepcd.1 . 2 (𝜑𝐴 <<s 𝐵)
2 ssltsepcd.2 . 2 (𝜑𝑋𝐴)
3 ssltsepcd.3 . 2 (𝜑𝑌𝐵)
4 ssltsepc 27154 . 2 ((𝐴 <<s 𝐵𝑋𝐴𝑌𝐵) → 𝑋 <s 𝑌)
51, 2, 3, 4syl3anc 1372 1 (𝜑𝑋 <s 𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5106   <s cslt 27005   <<s csslt 27142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-sslt 27143
This theorem is referenced by:  sslttr  27168  cofsslt  27259  coinitsslt  27260  cofcutrtime  27268  addsproplem2  27304  addsproplem4  27306  addsproplem5  27307  addsproplem6  27308  addsunif  27332  negsproplem2  27349  negsproplem4  27351  negsproplem5  27352  negsproplem6  27353  negsunif  27372  mulsproplem6  27406  mulsproplem7  27407  mulsproplem8  27408  mulsproplem9  27409
  Copyright terms: Public domain W3C validator